La composición de funciones suprayectivas es suprayectiva
Demostrar con Lean4 que la composición de funciones suprayectivas es suprayectiva.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 |
import Mathlib.Tactic open Function variable {α : Type _} {β : Type _} {γ : Type _} variable {f : α → β} {g : β → γ} example (hg : Surjective g) (hf : Surjective f) : Surjective (g ∘ f) := by sorry |
Demostración en lenguaje natural
Supongamos que \(f : A → B\) y \(g : B → C\) son suprayectivas. Tenemosque demostrar que
\[ (∀z ∈ C)(∃x ∈ A)[g(f(x)) = z] \]
Sea \(z ∈ C\). Por ser \(g\) suprayectiva, existe un \(y ∈ B\) tal que
\[ g(y) = z \tag{1} \]
Por ser \(f\) suprayectiva, existe un \(x ∈ A\) tal que
\[ f(x) = y \tag{2} \]
Por tanto,
\begin{align}
g(f(x)) &= g(y) &&\text{[por (2)]} \\
&= z &&\text{[por (1)]}
\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 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 |
import Mathlib.Tactic open Function variable {α : Type _} {β : Type _} {γ : Type _} variable {f : α → β} {g : β → γ} -- 1ª demostración example (hg : Surjective g) (hf : Surjective f) : Surjective (g ∘ f) := by intro z -- z : γ -- ⊢ ∃ a, (g ∘ f) a = z cases' hg z with y hy -- y : β -- hy : g y = z cases' hf y with x hx -- x : α -- hx : f x = y use x -- ⊢ (g ∘ f) x = z dsimp -- ⊢ g (f x) = z rw [hx] -- ⊢ g y = z exact hy -- 2ª demostración example (hg : Surjective g) (hf : Surjective f) : Surjective (g ∘ f) := by intro z -- z : γ -- ⊢ ∃ a, (g ∘ f) a = z cases' hg z with y hy -- y : β -- hy : g y = z cases' hf y with x hx -- x : α -- hx : f x = y use x -- ⊢ (g ∘ f) x = z dsimp -- ⊢ g (f x) = z rw [hx, hy] -- 3ª demostración example (hg : Surjective g) (hf : Surjective f) : Surjective (g ∘ f) := by intro z -- z : γ -- ⊢ ∃ a, (g ∘ f) a = z cases' hg z with y hy -- y : β -- hy : g y = z cases' hf y with x hx -- x : α -- hx : f x = y exact ⟨x, by dsimp ; rw [hx, hy]⟩ -- 4ª demostración example (hg : Surjective g) (hf : Surjective f) : Surjective (g ∘ f) := by intro z -- z : γ -- ⊢ ∃ a, (g ∘ f) a = z rcases hg z with ⟨y, hy : g y = z⟩ rcases hf y with ⟨x, hx : f x = y⟩ exact ⟨x, by dsimp ; rw [hx, hy]⟩ -- 5ª demostración example (hg : Surjective g) (hf : Surjective f) : Surjective (g ∘ f) := Surjective.comp hg hf -- Lemas usados -- ============ -- #check (Surjective.comp : Surjective g → Surjective f → Surjective (g ∘ f)) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 31.
