-
Notifications
You must be signed in to change notification settings - Fork 0
/
Introduccion_de_la_conjuncion.lean
142 lines (120 loc) · 2.63 KB
/
Introduccion_de_la_conjuncion.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
131
132
133
134
135
136
137
138
139
140
141
142
-- Introduccion_de_la_conjuncion.lean
-- {x ≤ y, y ≰ x} ⊢ x ≤ y ∧ x ≠ y
-- José A. Alonso Jiménez <https://jaalonso.github.io>
-- Sevilla, 11-diciembre-2023
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- Sean x e y dos números tales que
-- x ≤ y
-- ¬ y ≤ x
-- entonces
-- x ≤ y ∧ x ≠ y
-- ----------------------------------------------------------------------
-- Demostración en lenguaje natural
-- ================================
-- Como la conclusión es una conjunción, tenemos que desmostrar sus dos
-- partes. La primera parte (x ≤ y) coincide con la hipótesis. Para
-- demostrar la segunda parte (x ≠ y), supongamos que x = y; entonces
-- y ≤ x en contradicción con la segunda hipótesis.
-- Demostraciones con Lean4
-- ========================
import Mathlib.Data.Real.Basic
import Mathlib.Tactic
variable {x y : ℝ}
-- 1ª demostración
-- ===============
example
(h1 : x ≤ y)
(h2 : ¬y ≤ x)
: x ≤ y ∧ x ≠ y :=
by
constructor
. -- ⊢ x ≤ y
exact h1
. -- ⊢ x ≠ y
intro h3
-- h3 : x = y
-- ⊢ False
have h4 : y ≤ x := h3.symm.le
show False
exact h2 h4
-- 2ª demostración
-- ===============
example
(h1 : x ≤ y)
(h2 : ¬y ≤ x)
: x ≤ y ∧ x ≠ y :=
by
constructor
. -- ⊢ x ≤ y
exact h1
. -- ⊢ x ≠ y
intro h3
-- h3 : x = y
-- ⊢ False
exact h2 (h3.symm.le)
-- 3ª demostración
-- ===============
example
(h1 : x ≤ y)
(h2 : ¬y ≤ x)
: x ≤ y ∧ x ≠ y :=
⟨h1, fun h3 ↦ h2 (h3.symm.le)⟩
-- 4ª demostración
-- ===============
example
(h1 : x ≤ y)
(h2 : ¬y ≤ x)
: x ≤ y ∧ x ≠ y :=
by
constructor
. -- ⊢ x ≤ y
exact h1
. -- ⊢ x ≠ y
intro h3
-- h3 : x = y
-- ⊢ False
apply h2
-- ⊢ y ≤ x
rw [h3]
-- 5ª demostración
-- ===============
example
(h1 : x ≤ y)
(h2 : ¬y ≤ x)
: x ≤ y ∧ x ≠ y :=
by
constructor
. -- ⊢ x ≤ y
exact h1
. -- ⊢ x ≠ y
intro h3
-- h3 : x = y
-- ⊢ False
exact h2 (by rw [h3])
-- 6ª demostración
-- ===============
example
(h1 : x ≤ y)
(h2 : ¬ y ≤ x)
: x ≤ y ∧ x ≠ y :=
⟨h1, fun h ↦ h2 (by rw [h])⟩
-- 7ª demostración
-- ===============
example
(h1 : x ≤ y)
(h2 : ¬ y ≤ x)
: x ≤ y ∧ x ≠ y :=
by
have h3 : x ≠ y
. contrapose! h2
-- ⊢ y ≤ x
rw [h2]
exact ⟨h1, h3⟩
-- 8ª demostración
-- ===============
example
(h1 : x ≤ y)
(h2 : ¬ y ≤ x)
: x ≤ y ∧ x ≠ y :=
by aesop