-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathCN_de_monotona.lean
103 lines (86 loc) · 2.27 KB
/
CN_de_monotona.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
-- CN_de_monotona.lean
-- Si f es monótona y f(a) < f(b), entonces a < b.
-- José A. Alonso Jiménez <https://jaalonso.github.io>
-- Sevilla, 21-noviembre-2023
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- Demostrar que si f es monótona y f(a) < f(b), entonces a < b
-- ----------------------------------------------------------------------
-- Demostración en lenguaje natural
-- ================================
-- Usaremos los lemas
-- a ≱ b → a < b (L1)
-- a ≥ b → a ≮ b (L2)
--
-- Usando el lema L1, basta demostrar que a ≱ b. Lo haremos por
-- reducción al absurdo. Para ello, supongamos que a ≥ b. Como f es
-- monótona, se tiene que f(a) ≥ f(b) y, aplicando el lema L2,
-- f(a) ≮ f(b), que contradice a la hipótesis.
-- Demostraciones con Lean4
-- ========================
import Mathlib.Data.Real.Basic
variable (f : ℝ → ℝ)
variable (a b : ℝ)
-- 1ª demostración
-- ===============
example
(h1 : Monotone f)
(h2 : f a < f b)
: a < b :=
by
apply lt_of_not_ge
-- ⊢ ¬a ≥ b
intro h3
-- h3 : a ≥ b
-- ⊢ False
have h4 : f a ≥ f b := h1 h3
have h5 : ¬ f a < f b := not_lt_of_ge h4
exact h5 h2
-- 2ª demostración
-- ===============
example
(h1 : Monotone f)
(h2 : f a < f b)
: a < b :=
by
apply lt_of_not_ge
-- ⊢ ¬a ≥ b
intro h3
-- h3 : a ≥ b
-- ⊢ False
have h5 : ¬ f a < f b := not_lt_of_ge (h1 h3)
exact h5 h2
-- 3ª demostración
-- ===============
example
(h1 : Monotone f)
(h2 : f a < f b)
: a < b :=
by
apply lt_of_not_ge
-- ⊢ ¬a ≥ b
intro h3
-- h3 : a ≥ b
-- ⊢ False
exact (not_lt_of_ge (h1 h3)) h2
-- 4ª demostración
-- ===============
example
(h1 : Monotone f)
(h2 : f a < f b)
: a < b :=
by
apply lt_of_not_ge
-- ⊢ ¬a ≥ b
exact fun h3 ↦ (not_lt_of_ge (h1 h3)) h2
-- 5ª demostración
-- ===============
example
(h1 : Monotone f)
(h2 : f a < f b)
: a < b :=
lt_of_not_ge (fun h3 ↦ (not_lt_of_ge (h1 h3)) h2)
-- Lemas usados
-- ============
-- #check (lt_of_not_ge : ¬ a ≥ b → a < b)
-- #check (not_lt_of_ge : a ≥ b → ¬ a < b)