Demostrar con Lean4 que en los órdenes parciales, \[a < b ↔ a ≤ b ∧ a ≠ b\]
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Tactic variable {α : Type _} [PartialOrder α] variable (a b : α) example : a < b ↔ a ≤ b ∧ a ≠ b := by sorry
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:
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