Supremum_of_Subset
Provedorder-theoryproofwiki
Let be an ordered set. Let . Let . Let admit a supremum (in ). If also admits a supremum (in ), then .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic theorem Supremum_of_Subset (S T : Set ℝ) (hTS : T ⊆ S) (hS : BddAbove S) (hT : T.Nonempty) : sSup T ≤ sSup S := by sorry
Source