-
Notifications
You must be signed in to change notification settings - Fork 0
/
Principio_de_explosion.lean
81 lines (63 loc) · 1.51 KB
/
Principio_de_explosion.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
-- Principio_de_explosion.lean
-- Si 0 < 0, entonces a > 37 para cualquier número a.
-- José A. Alonso Jiménez <https://jaalonso.github.io>
-- Sevilla, 8-diciembre-2023
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- Demostrar que si 0 < 0, entonces a > 37 para cualquier número a.
-- ----------------------------------------------------------------------
-- Demostración en lenguaje natural
-- ================================
-- Basta demostrar una contradicción, ya que de una contradicción se
-- sigue cualquier cosa.
--
-- La hipótesis es una contradicción con la propiedad irreflexiva de la
-- relación <.
-- Demostraciones con Lean4
-- ========================
import Mathlib.Tactic
variable (a : ℝ)
-- 1ª demostración
-- ===============
example
(h : 0 < 0)
: a > 37 :=
by
exfalso
-- ⊢ False
show False
exact lt_irrefl 0 h
-- 2ª demostración
-- ===============
example
(h : 0 < 0)
: a > 37 :=
by
exfalso
-- ⊢ False
apply lt_irrefl 0 h
-- 3ª demostración
-- ===============
example
(h : 0 < 0)
: a > 37 :=
absurd h (lt_irrefl 0)
-- 4ª demostración
-- ===============
example
(h : 0 < 0)
: a > 37 :=
by
have : ¬ 0 < 0 := lt_irrefl 0
contradiction
-- 5ª demostración
-- ===============
example
(h : 0 < 0)
: a > 37 :=
by linarith
-- Lemas usados
-- ============
-- variable (p q : Prop)
-- #check (lt_irrefl a : ¬a < a)
-- #check (absurd : p → ¬p → q)