Demostrar con Lean4 que la composición de funciones inyectivas es inyectiva.
Para ello, completar la siguiente teoría de Lean4:
|
|
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)
y tenemos que demostrar que
x=y
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
