La composición de funciones inyectivas es inyectiva
Demostrar con Lean4 que la composición de funciones inyectivas es inyectiva.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 12 |
import Mathlib.Tactic open Function variable {α : Type _} {β : Type _} {γ : Type _} variable {f : α → β} {g : β → γ} example (hg : Injective g) (hf : Injective f) : Injective (g ∘ f) := by sorry |
Demostraciones en lenguaje natural (LN)
1ª demostración en LN
Tenemos que demostrar que
\[ (∀ x, y) [(g ∘ f)(x) = (g ∘ f)(y) → x = y] \]
Sean \(x, y\) tales que
\[ (g ∘ f)(x) = (g ∘ f)(y) \]
Entonces, por la definición de la composición,
\[ g(f(x)) = g(f(y)) \]
y, ser \(g\) inyectiva,
\[ f(x) = f(y) \]
y, ser \(f\) inyectiva,
\[ x = y \]
2ª demostración en LN
Tenemos que demostrar que
\[ (∀ x, y) [(g ∘ f)(x) = (g ∘ f)(y) → x = y] \]
Sean \(x, y\) tales que
\[ (g ∘ f)(x) = (g ∘ f)(y) \tag{1} \]
y tenemos que demostrar que
\[ x = y \tag{2} \]
El objetivo (2), usando que \(f\) es inyectiva, se reduce a
\[ f(x) = f(y) \]
que, usando que \(g\) es inyectiva, se reduce a
\[ g(f(x)) = g(f(y)) \]
que, por la definición de la composición, coincide con (1).
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 |
import Mathlib.Tactic open Function variable {α : Type _} {β : Type _} {γ : Type _} variable {f : α → β} {g : β → γ} -- 1ª demostración (basada en la 1ª en LN) example (hg : Injective g) (hf : Injective f) : Injective (g ∘ f) := by intro (x : α) (y : α) (h1: (g ∘ f) x = (g ∘ f) y) have h2: g (f x) = g (f y) := h1 have h3: f x = f y := hg h2 show x = y exact hf h3 -- 2ª demostración example (hg : Injective g) (hf : Injective f) : Injective (g ∘ f) := by intro (x : α) (y : α) (h1: (g ∘ f) x = (g ∘ f) y) have h2: f x = f y := hg h1 show x = y exact hf h2 -- 3ª demostración example (hg : Injective g) (hf : Injective f) : Injective (g ∘ f) := by intro x y h exact hf (hg h) -- 4ª demostración example (hg : Injective g) (hf : Injective f) : Injective (g ∘ f) := fun _ _ h ↦ hf (hg h) -- 5ª demostración (basada en la 2ª en LN) example (hg : Injective g) (hf : Injective f) : Injective (g ∘ f) := by intros x y h -- x y : α -- h : (g ∘ f) x = (g ∘ f) y apply hf -- ⊢ f x = f y apply hg -- ⊢ g (f x) = g (f y) apply h -- 6ª demostración example (hg : Injective g) (hf : Injective f) : Injective (g ∘ f) := -- by exact? Injective.comp hg hf -- 7ª demostración example (hg : Injective g) (hf : Injective f) : Injective (g ∘ f) := by tauto -- Lemas usados -- ============ -- #check (Injective.comp : Injective g → Injective f → Injective (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. 28.
