En ℝ, a < b → ¬(b < a)
Demostrar con Lean4 que en \(ℝ\), \(a < b → ¬(b < a)\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Data.Real.Basic variable (a b : ℝ) example (h : a < b) : ¬ b < a := by sorry |
Demostración en lenguaje natural
Por hipótesis \(a < b\) y tenemos que demostrar que \(¬(b < a)\). Supongamos que \(b < a\). Entonces, por la propiedad transiva \(a < a\) que es una contradicción con la propiedad irreflexiva.
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 |
import Mathlib.Data.Real.Basic variable (a b : ℝ) -- 1ª demostración example (h : a < b) : ¬ b < a := by intro h1 -- h1 : b < a -- ⊢ False have : a < a := lt_trans h h1 apply lt_irrefl a this -- 2ª demostración example (h : a < b) : ¬ b < a := by intro h1 -- h1 : b < a -- ⊢ False exact lt_irrefl a (lt_trans h h1) -- 3ª demostración example (h : a < b) : ¬ b < a := fun h1 ↦ lt_irrefl a (lt_trans h h1) -- 4ª demostración example (h : a < b) : ¬ b < a := lt_asymm h -- Lemas usados -- ============ -- variable (c : ℝ) -- #check (lt_asymm : a < b → ¬b < a) -- #check (lt_irrefl a : ¬a < a) -- #check (lt_trans : a < b → b < c → a < c) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 32.
