-
Notifications
You must be signed in to change notification settings - Fork 0
/
Las_funciones_biyectivas_tienen_inversa.lean
87 lines (77 loc) · 1.94 KB
/
Las_funciones_biyectivas_tienen_inversa.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
-- Las_funciones_biyectivas_tienen_inversa.lean
-- Las funciones biyectivas tienen inversa
-- José A. Alonso Jiménez
-- Sevilla, 9 de agosto de 2021
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- En Lean 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)
-- y que f tiene inversa por
-- def tiene_inversa (f : X → Y) :=
-- ∃ g, inversa f g
--
-- Demostrar que si la función f es biyectiva, entonces f tiene inversa.
-- ---------------------------------------------------------------------
import tactic
open function
variables {X Y : Type*}
variable (f : X → Y)
def inversa (f : X → Y) (g : Y → X) :=
(∀ x, (g ∘ f) x = x) ∧ (∀ y, (f ∘ g) y = y)
def tiene_inversa (f : X → Y) :=
∃ g, inversa g f
-- 1ª demostración
example
(hf : bijective f)
: tiene_inversa f :=
begin
rcases hf with ⟨hfiny, hfsup⟩,
choose g hg using hfsup,
use g,
split,
{ exact hg, },
{ intro a,
apply hfiny,
rw hg (f a), },
end
-- 2ª demostración
example
(hf : bijective f)
: tiene_inversa f :=
begin
rcases hf with ⟨hfiny, hfsup⟩,
choose g hg using hfsup,
use g,
split,
{ exact hg, },
{ intro a,
exact @hfiny (g (f a)) a (hg (f a)), },
end
-- 3ª demostración
example
(hf : bijective f)
: tiene_inversa f :=
begin
rcases hf with ⟨hfiny, hfsup⟩,
choose g hg using hfsup,
use g,
exact ⟨hg, λ a, @hfiny (g (f a)) a (hg (f a))⟩,
end
-- 4ª demostración
example
(hf : bijective f)
: tiene_inversa f :=
begin
rcases hf with ⟨hfiny, hfsup⟩,
choose g hg using hfsup,
use [g, ⟨hg, λ a, @hfiny (g (f a)) a (hg (f a))⟩],
end
-- 5ª demostración
example
(hf : bijective f)
: tiene_inversa f :=
begin
cases (bijective_iff_has_inverse.mp hf) with g hg,
by tidy,
end