-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathLa_inversa_de_una_funcion_biyectiva_es_biyectiva.lean
130 lines (109 loc) · 3.51 KB
/
La_inversa_de_una_funcion_biyectiva_es_biyectiva.lean
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
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
-- La_inversa_de_una_funcion_biyectiva_es_biyectiva.lean
-- La inversa de una función es biyectiva.
-- José A. Alonso Jiménez <https://jaalonso.github.io>
-- Sevilla, 19-junio-2024
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- En Lean4 se puede definir que g es una inversa de f por
-- def inversa (f : X → Y) (g : Y → X) :=
-- (∀ x, (g ∘ f) x = x) ∧ (∀ y, (f ∘ g) y = y)
--
-- Demostrar que si g es una inversa de f, entonces g es biyectiva.
-- ---------------------------------------------------------------------
-- Demostración en lenguaje natural
-- ================================
-- Para demostrar que g: Y → X es biyectiva, basta probar que existe una
-- h que es inversa de g por la izquierda y por la derecha; es decir,
-- (∀y ∈ Y)[(h ∘ g)(y) = y] (1)
-- (∀x ∈ X)[(g ∘ h)(x) = x] (2)
--
-- Puesto que g es una inversa de f, entonces
-- (∀x ∈ X)[(g ∘ f)(x) = x] (3)
-- (∀y ∈ Y)[(f ∘ g)(y) = y] (4)
--
-- Tomando f como h, (1) se verifica por (4) y (2) se verifica por (3).
-- Demostraciones con Lean4
-- ========================
import Mathlib.Tactic
open Function
variable {X Y : Type _}
variable (f : X → Y)
variable (g : Y → X)
def inversa (f : X → Y) (g : Y → X) :=
(∀ x, (g ∘ f) x = x) ∧ (∀ y, (f ∘ g) y = y)
-- 1ª demostración
-- ===============
example
(hg : inversa g f)
: Bijective g :=
by
rcases hg with ⟨h1, h2⟩
-- h1 : ∀ (x : Y), (f ∘ g) x = x
-- h2 : ∀ (y : X), (g ∘ f) y = y
rw [bijective_iff_has_inverse]
-- ⊢ ∃ g_1, LeftInverse g_1 g ∧ Function.RightInverse g_1 g
use f
-- ⊢ LeftInverse f g ∧ Function.RightInverse f g
constructor
. -- ⊢ LeftInverse f g
exact h1
. -- ⊢ Function.RightInverse f g
exact h2
-- 2ª demostración
-- ===============
example
(hg : inversa g f)
: Bijective g :=
by
rcases hg with ⟨h1, h2⟩
-- h1 : ∀ (x : Y), (f ∘ g) x = x
-- h2 : ∀ (y : X), (g ∘ f) y = y
rw [bijective_iff_has_inverse]
-- ⊢ ∃ g_1, LeftInverse g_1 g ∧ Function.RightInverse g_1 g
use f
-- ⊢ LeftInverse f g ∧ Function.RightInverse f g
exact ⟨h1, h2⟩
-- 3ª demostración
-- ===============
example
(hg : inversa g f)
: Bijective g :=
by
rcases hg with ⟨h1, h2⟩
-- h1 : ∀ (x : Y), (f ∘ g) x = x
-- h2 : ∀ (y : X), (g ∘ f) y = y
rw [bijective_iff_has_inverse]
-- ⊢ ∃ g_1, LeftInverse g_1 g ∧ Function.RightInverse g_1 g
exact ⟨f, ⟨h1, h2⟩⟩
-- 4ª demostración
-- ===============
example
(hg : inversa g f)
: Bijective g :=
by
rw [bijective_iff_has_inverse]
-- ⊢ ∃ g_1, LeftInverse g_1 g ∧ Function.RightInverse g_1 g
use f
-- ⊢ LeftInverse f g ∧ Function.RightInverse f g
exact hg
-- 5ª demostración
-- ===============
example
(hg : inversa g f)
: Bijective g :=
by
rw [bijective_iff_has_inverse]
-- ⊢ ∃ g_1, LeftInverse g_1 g ∧ Function.RightInverse g_1 g
exact ⟨f, hg⟩
-- 6ª demostración
-- ===============
example
(hg : inversa g f)
: Bijective g :=
by
apply bijective_iff_has_inverse.mpr
-- ⊢ ∃ g_1, LeftInverse g_1 g ∧ Function.RightInverse g_1 g
exact ⟨f, hg⟩
-- Lemas usados
-- ============
-- #check (bijective_iff_has_inverse : Bijective f ↔ ∃ g, LeftInverse g f ∧ RightInverse g f)