Si c ≠ 0, entonces la función (x ↦ cx + d) es suprayectiva
Demostrar con Lean4 que si \(c ≠ 0\), entonces la función \(x ↦ cx + d\) 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 d : ℝ} open Function example (h : c ≠ 0) : Surjective (fun x ↦ c * x + d) := by sorry |
Demostración en lenguaje natural
Hay que demostrar que
\[ (∀x ∈ ℝ)(∃y ∈ ℝ)[cy+d = x] \]
Para \(x ∈ ℝ\), sea \(y = \dfrac{x-d}{c}\). Entonces,
\begin{align}
cy &= c\left(\frac{x-d}{c}\right)+d \\
&= (x-d)+d \\
&= x
\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 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 |
import Mathlib.Data.Real.Basic variable {c d : ℝ} open Function -- 1ª demostración -- =============== example (h : c ≠ 0) : Surjective (fun x ↦ c * x + d) := by intro x -- x : ℝ -- ⊢ ∃ a, (fun x => c * x + d) a = x use ((x - d) / c) -- ⊢ (fun x => c * x + d) ((x - d) / c) = x dsimp -- ⊢ c * ((x - d) / c) + d = x show c * ((x - d) / c) + d = x calc c * ((x - d) / c) + d = (x - d) + d := congrArg (. + d) (mul_div_cancel' (x - d) h) _ = x := sub_add_cancel x d -- 2ª demostración -- =============== example (h : c ≠ 0) : Surjective (fun x ↦ c * x + d) := by intro x -- x : ℝ -- ⊢ ∃ a, (fun x => c * x + d) a = x use ((x - d) / c) -- ⊢ (fun x => c * x + d) ((x - d) / c) = x dsimp -- ⊢ c * ((x - d) / c) + d = x simp [mul_div_cancel', h] -- 3ª demostración -- =============== example (h : c ≠ 0) : Surjective (fun x ↦ c * x + d) := by intro x -- x : ℝ -- ⊢ ∃ a, (fun x => c * x + d) a = x use ((x - d) / c) -- ⊢ (fun x => c * x + d) ((x - d) / c) = x simp [mul_div_cancel', h] -- 4ª demostración -- =============== example (h : c ≠ 0) : Surjective (fun x ↦ c * x + d) := fun x ↦ ⟨(x - d) / c, by simp [mul_div_cancel', h]⟩ -- Lemas usados -- ============ -- variable (a b : ℝ) -- #check (mul_div_cancel' a : b ≠ 0 → b * (a / b) = a) -- #check (sub_add_cancel a b : a - b + b = a) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 32.
