Si c ≠ 0, entonces la función (x ↦ cx) es suprayectiva
Demostrar con Lean4 que si \(c ≠ 0\), entonces la función \(x ↦ cx\) es suprayectiva.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Data.Real.Basic variable {c : ℝ} open Function example (h : c ≠ 0) : Surjective (fun x ↦ c * x) := by sorry |
Demostración en lenguaje natural
Hay que demostrar que
\[ (∀ x ∈ ℝ)(∃ y ∈ ℝ)[cy = x] \]
Sea \(x ∈ ℝ\). Entonces, \(y = x/c ∈ R\) y
\begin{align}
cy &= c(x/c) \\
&= y
\end{align}
Demostraciones con Lean4
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 |
import Mathlib.Data.Real.Basic variable {c : ℝ} open Function -- 1ª demostración example (h : c ≠ 0) : Surjective (fun x ↦ c * x) := by intro x -- x : ℝ -- ⊢ ∃ a, (fun x => c * x) a = x use (x / c) -- ⊢ (fun x => c * x) (x / c) = x dsimp -- ⊢ c * (x / c) = x rw [mul_comm] -- ⊢ (x / c) * c = x exact div_mul_cancel x h -- 2ª demostración example (h : c ≠ 0) : Surjective (fun x ↦ c * x) := by intro x -- x : ℝ -- ⊢ ∃ a, (fun x => c * x) a = x use (x / c) -- ⊢ (fun x => c * x) (x / c) = x exact mul_div_cancel' x h -- 3ª demostración example (h : c ≠ 0) : Surjective (fun x ↦ c * x) := fun x ↦ ⟨x / c, mul_div_cancel' x h⟩ -- 4ª demostración example (h : c ≠ 0) : Surjective (fun x ↦ c * x) := mul_left_surjective₀ h -- Lemas usados -- ============ -- variable (a b : ℝ) -- #check (div_mul_cancel a : b ≠ 0 → (a / b) * b = a) -- #check (mul_comm a b : a * b = b * a) -- #check (mul_div_cancel' a : b ≠ 0 → b * (a / b) = a) -- #check (mul_left_surjective₀ : c ≠ 0 → Surjective (fun x ↦ c * x)) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 31.
