Si a es una cota superior de s y a ≤ b, entonces b es una cota superior de s
Demostrar que si a es una cota superior de s y a ≤ b, entonces b es una cota superior de s
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 |
import tactic variables {α : Type*} [partial_order α] variables s : set α variables a b : α -- (cota_superior s a) expresa que a es una cota superior de s. def cota_superior (s : set α) (a : α) := ∀ {x}, x ∈ s → x ≤ a example (h1 : cota_superior s a) (h2 : a ≤ b) : cota_superior s b := 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 |
import tactic variables {α : Type*} [partial_order α] variables s : set α variables a b : α -- (cota_superior s a) expresa que a es una cota superior de s. def cota_superior (s : set α) (a : α) := ∀ {x}, x ∈ s → x ≤ a -- 1ª demostración -- =============== example (h1 : cota_superior s a) (h2 : a ≤ b) : cota_superior s b := begin intro x, assume xs : x ∈ s, have h3 : x ≤ a := h1 xs, show x ≤ b, by exact le_trans h3 h2, end -- 2ª demostración -- =============== example (h1 : cota_superior s a) (h2 : a ≤ b) : cota_superior s b := begin intros x xs, calc x ≤ a : h1 xs ... ≤ b : h2 end |
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, p. 29.
