Si a, b, c, d, e ∈ ℝ tales que a ≤ b, b < c, c ≤ d, d < e, entonces a < e
Demostrar que si a, b, c, d, e ∈ ℝ tales que
|
1 2 3 4 |
a ≤ b b < c c ≤ d d < e |
entonces
|
1 |
a < e |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 10 11 |
import data.real.basic variables a b c d e : ℝ example (h₀ : a ≤ b) (h₁ : b < c) (h₂ : c ≤ d) (h₃ : d < e) : a < e := sorry |
Soluciones con 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 |
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 := calc a ≤ b : h₀ ... < c : h₁ ... ≤ d : h₂ ... < e : h₃ -- 2ª 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 -- 3ª demostración -- =============== example (h₀ : a ≤ b) (h₁ : b < c) (h₂ : c ≤ d) (h₃ : d < e) : a < e := by finish -- 4ª demostración -- =============== example (h₀ : a ≤ b) (h₁ : b < c) (h₂ : c ≤ d) (h₃ : d < e) : a < e := by linarith |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
Referencias
- J. Avigad, K. Buzzard, R.Y. Lewis y P. Massot. Mathematics in Lean.
