Si a es una cota superior de s y a ≤ b, entonces b es una cota superior de s
Demostrar con Lean4 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 Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 |
import Mathlib.Tactic variable {α : Type _} [PartialOrder α] variable (s : Set α) variable (a b : α) -- (CotaSupConj s a) afirma que a es una cota superior del conjunto s. def CotaSupConj (s : Set α) (a : α) := ∀ {x}, x ∈ s → x ≤ a example (h1 : CotaSupConj s a) (h2 : a ≤ b) : CotaSupConj s b := by sorry |
Demostración en lenguaje natural
Tenemos que demostrar que
\[ (∀ x) [x ∈ s → x ≤ b] \]
Sea \(x\) tal que \(x ∈ s\). Entonces,
\begin{align}
x &≤ a &&\text{[porque \(a\) es una cota superior de \(s\)]} \\
&≤ b
\end{align}
Por tanto, \(x ≤ b\).
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 |
import Mathlib.Tactic variable {α : Type _} [PartialOrder α] variable (s : Set α) variable (a b : α) -- (CotaSupConj s a) afirma que a es una cota superior del conjunto s. def CotaSupConj (s : Set α) (a : α) := ∀ {x}, x ∈ s → x ≤ a -- 1ª demostración example (h1 : CotaSupConj s a) (h2 : a ≤ b) : CotaSupConj s b := by intro x (xs : x ∈ s) have h3 : x ≤ a := h1 xs show x ≤ b exact le_trans h3 h2 -- 2ª demostración example (h1 : CotaSupConj s a) (h2 : a ≤ b) : CotaSupConj s b := by intro x (xs : x ∈ s) calc x ≤ a := h1 xs _ ≤ b := h2 - -- Lemas usados -- ============ -- variable (c : α) -- #check (le_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. 27.
