La función (x ↦ x + c) es suprayectiva
Demostrar con Lean4 que la función \(x ↦ x + c\) es suprayectiva.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Data.Real.Basic variable {c : ℝ} open Function example : Surjective (fun x ↦ x + c) := by sorry |
Demostración en lenguaje natural
Tenemos que demostrar que
\[ (∀ x ∈ ℝ)(∃ y ∈ ℝ)[y+c = x] \]
Sea \(x ∈ ℝ\). Entonces, \(y = x-c ∈ ℝ\) y
\begin{align}
y + c &= (x – c) + c \\
&= 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 |
import Mathlib.Data.Real.Basic variable {c : ℝ} open Function -- 1ª demostración example : Surjective (fun x ↦ x + c) := by intro x -- x : ℝ -- ⊢ ∃ a, (fun x => x + c) a = x use x - c -- ⊢ (fun x => x + c) (x - c) = x dsimp -- ⊢ (x - c) + c = x exact sub_add_cancel x c -- 2ª demostración example : Surjective (fun x ↦ x + c) := by intro x -- x : ℝ -- ⊢ ∃ a, (fun x => x + c) a = x use x - c -- ⊢ (fun x => x + c) (x - c) = x change (x - c) + c = x -- ⊢ (x - c) + c = x exact sub_add_cancel x c -- 3ª demostración example : Surjective (fun x ↦ x + c) := by intro x -- x : ℝ -- ⊢ ∃ a, (fun x => x + c) a = x use x - c -- ⊢ (fun x => x + c) (x - c) = x exact sub_add_cancel x c -- 4ª demostración example : Surjective (fun x ↦ x + c) := fun x ↦ ⟨x - c, sub_add_cancel x c⟩ -- 5ª demostración example : Surjective (fun x ↦ x + c) := fun x ↦ ⟨x - c, by ring⟩ -- 6ª demostración example : Surjective (fun x ↦ x + c) := add_right_surjective c -- Lemas usados -- ============ -- variable (a b : ℝ) -- #check (sub_add_cancel a b : (a - b) + b = a) -- #check (add_right_surjective c : Surjective (fun x ↦ x + c)) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 31.
