Si 0 < 0, entonces a > 37 para cualquier número a
Demostrar con Lean4 que si \(0 < 0\), entonces \(a > 37\) para cualquier número \(a\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Tactic variable (a : ℕ) example (h : 0 < 0) : a > 37 := by sorry |
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
|
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 |
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) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 34.
