-
Notifications
You must be signed in to change notification settings - Fork 1
/
Ejercicio_sobre_orden.lean
74 lines (64 loc) · 1.24 KB
/
Ejercicio_sobre_orden.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
-- ---------------------------------------------------------------------
-- Ejercicio. Demostrar que si a, b, c, d y e son números reales tales
-- que
-- a ≤ b
-- b < c
-- c ≤ d
-- d < e
-- entonces
-- a < e
-- ----------------------------------------------------------------------
import data.real.basic
variables a b c d e : ℝ
-- 1ª demostración
-- ===============
example
(h₀ : a ≤ b)
(h₁ : b < c)
(h₂ : c ≤ d)
(h₃ : d < e) :
a < e :=
begin
apply lt_of_le_of_lt h₀,
apply lt_trans h₁,
apply lt_of_le_of_lt h₂,
exact h₃,
end
-- El desarrollo de la prueba es
--
-- a b c d e : ℝ,
-- h₀ : a ≤ b,
-- h₁ : b < c,
-- h₂ : c ≤ d,
-- h₃ : d < e
-- ⊢ a < e
-- apply lt_of_le_of_lt h₀,
-- ⊢ b < e
-- apply lt_trans h₁,
-- ⊢ c < e
-- apply lt_of_le_of_lt h₂,
-- ⊢ d < e
-- exact h₃,
-- no goals
-- 2ª demostración
-- ===============
example
(h₀ : a ≤ b)
(h₁ : b < c)
(h₂ : c ≤ d)
(h₃ : d < e) :
a < e :=
calc
a ≤ b : h₀
... < c : h₁
... ≤ d : h₂
... < e : h₃
-- 3ª demostración
-- ===============
example
(h₀ : a ≤ b)
(h₁ : b < c)
(h₂ : c ≤ d)
(h₃ : d < e) :
a < e :=
by finish