-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathPreorden_transitiva.lean
126 lines (107 loc) · 4.05 KB
/
Preorden_transitiva.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
-- Preorden_transitiva.lean
-- Si ≤ es un preorden, entonces < es transitiva.
-- José A. Alonso Jiménez <https://jaalonso.github.io>
-- Sevilla, 5-enero-2024
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- Demostrar que si ≤ es un preorden, entonces < es transitiva.
-- ----------------------------------------------------------------------
-- Demostración en lenguaje natural
-- ================================
-- Se usará la siguiente propiedad de los preórdenes
-- (∀ a, b)[a < b ↔ a ≤ b ∧ b ≰ a]
-- Con dicha propiedad, lo que tenemos que demostrar se transforma en
-- a ≤ b ∧ b ≰ a → b ≤ c ∧ c ≰ b → a ≤ c ∧ c ≰ a
-- Para demostrarla, supongamos que
-- a ≤ b (1)
-- b ≰ a (2)
-- b ≤ c (3)
-- c ≰ b (4)
-- y tenemos que demostrar las siguientes relaciones
-- a ≤ c (5)
-- c ≰ a (6)
--
-- La (5) se tiene aplicando la propiedad transitiva a (1) y (3).
--
-- Para demostrar la (6), supongamos que
-- c ≤ a (7)
-- entonces, junto a la (1), por la propieda transitiva se tiene
-- c ≤ b
-- que es una contradicción con la (4).
-- Demostraciones con Lean4
-- ========================
import Mathlib.Tactic
variable {α : Type _} [Preorder α]
variable (a b c : α)
-- 1ª demostración
-- ===============
example : a < b → b < c → a < c :=
by
simp only [lt_iff_le_not_le]
-- ⊢ a ≤ b ∧ ¬b ≤ a → b ≤ c ∧ ¬c ≤ b → a ≤ c ∧ ¬c ≤ a
rintro ⟨h1 : a ≤ b, _h2 : ¬b ≤ a⟩ ⟨h3 : b ≤ c, h4 : ¬c ≤ b⟩
-- ⊢ a ≤ c ∧ ¬c ≤ a
constructor
. -- ⊢ a ≤ c
exact le_trans h1 h3
. -- ⊢ ¬c ≤ a
contrapose! h4
-- h4 : c ≤ a
-- ⊢ c ≤ b
exact le_trans h4 h1
-- 2ª demostración
-- ===============
example : a < b → b < c → a < c :=
by
simp only [lt_iff_le_not_le]
-- ⊢ a ≤ b ∧ ¬b ≤ a → b ≤ c ∧ ¬c ≤ b → a ≤ c ∧ ¬c ≤ a
rintro ⟨h1 : a ≤ b, _h2 : ¬b ≤ a⟩ ⟨h3 : b ≤ c, h4 : ¬c ≤ b⟩
-- ⊢ a ≤ c ∧ ¬c ≤ a
constructor
. -- ⊢ a ≤ c
exact le_trans h1 h3
. -- ⊢ ¬c ≤ a
rintro (h5 : c ≤ a)
-- ⊢ False
have h6 : c ≤ b := le_trans h5 h1
show False
exact h4 h6
-- 3ª demostración
-- ===============
example : a < b → b < c → a < c :=
by
simp only [lt_iff_le_not_le]
-- ⊢ a ≤ b ∧ ¬b ≤ a → b ≤ c ∧ ¬c ≤ b → a ≤ c ∧ ¬c ≤ a
rintro ⟨h1 : a ≤ b, _h2 : ¬b ≤ a⟩ ⟨h3 : b ≤ c, h4 : ¬c ≤ b⟩
-- ⊢ a ≤ c ∧ ¬c ≤ a
constructor
. -- ⊢ a ≤ c
exact le_trans h1 h3
. -- ⊢ ¬c ≤ a
exact fun h5 ↦ h4 (le_trans h5 h1)
-- 4ª demostración
-- ===============
example : a < b → b < c → a < c :=
by
simp only [lt_iff_le_not_le]
-- ⊢ a ≤ b ∧ ¬b ≤ a → b ≤ c ∧ ¬c ≤ b → a ≤ c ∧ ¬c ≤ a
rintro ⟨h1 : a ≤ b, _h2 : ¬b ≤ a⟩ ⟨h3 : b ≤ c, h4 : ¬c ≤ b⟩
-- ⊢ a ≤ c ∧ ¬c ≤ a
exact ⟨le_trans h1 h3, fun h5 ↦ h4 (le_trans h5 h1)⟩
-- 5ª demostración
-- ===============
example : a < b → b < c → a < c :=
by
simp only [lt_iff_le_not_le]
-- ⊢ a ≤ b ∧ ¬b ≤ a → b ≤ c ∧ ¬c ≤ b → a ≤ c ∧ ¬c ≤ a
exact fun ⟨h1, _h2⟩ ⟨h3, h4⟩ ↦ ⟨le_trans h1 h3,
fun h5 ↦ h4 (le_trans h5 h1)⟩
-- 6ª demostración
-- ===============
example : a < b → b < c → a < c :=
lt_trans
-- Lemas usados
-- ============
-- #check (lt_iff_le_not_le : a < b ↔ a ≤ b ∧ ¬b ≤ a)
-- #check (le_trans : a ≤ b → b ≤ c → a ≤ c)
-- #check (lt_trans : a < b → b < c → a < c)