-
Notifications
You must be signed in to change notification settings - Fork 1
/
Teorema_de_Cantor.lean
70 lines (64 loc) · 1.4 KB
/
Teorema_de_Cantor.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
-- ---------------------------------------------------------------------
-- Ejercicio. Demostrar el teorema de Cantor: No existe singuna
-- aplicación suprayectiva de un conjunto en su conjunto potencia.
-- ----------------------------------------------------------------------
import data.set.basic
open function
variable {α : Type*}
theorem Cantor : ∀ f : α → set α, ¬ surjective f :=
begin
intros f surjf,
let S := {i | i ∉ f i},
cases surjf S with j hj,
have h₁ : j ∉ f j,
{ intro h',
have : j ∉ f j,
{ by rwa hj at h' },
contradiction },
have h₂ : j ∈ S,
from h₁,
have h₃ : j ∉ S,
by rwa hj at h₁,
contradiction,
end
-- Prueba
-- ======
/-
α : Type u_1
⊢ ∀ (f : α → set α), ¬surjective f
>> intros f surjf,
f : α → set α,
surjf : surjective f
⊢ false
>> let S := { i | i ∉ f i},
S : set α := {i : α | i ∉ f i}
⊢ false
>> rcases surjf S with j,
j : α,
h : f j = S
⊢ false
>> have h₁ : j ∉ f j,
| ⊢ j ∉ f j
| >> { intro h',
| h' : j ∈ f j
| ⊢ false
| >> have : j ∉ f j,
| | ⊢ j ∉ f j
| | >> { by rwa h at h' },
| this : j ∉ f j
| ⊢ false
| >> contradiction },
h₁ : j ∉ f j
⊢ false
>> have h₂ : j ∈ S,
| ⊢ j ∈ S
| >> from h₁,
h₂ : j ∈ S
⊢ false
>> have h₃ : j ∉ S,
>> by rwa h at h₁,
h₃ : j ∉ S
⊢ false
>> contradiction,
no goals
-/