English
If every element of s is principal for op, then the supremum is principal: Principal op (sSup s).
Русский
Если каждый элемент множества s является principal для op, то их верхняя граница также principal: Principal op (sSup s).
LaTeX
$$$$ \forall {s : Set Ordinal}, ( \forall x \in s, \operatorname{Principal}(op) x ) \Rightarrow \operatorname{Principal}(op) (\operatorname{csSup} s). $$$$
Lean4
protected theorem sSup {s : Set Ordinal} (H : ∀ x ∈ s, Principal op x) : Principal op (sSup s) :=
by
have : Principal op (sSup ∅) := by simp
by_cases hs : BddAbove s
· obtain rfl | hs' := s.eq_empty_or_nonempty
· assumption
simp only [Principal, lt_csSup_iff hs hs', forall_exists_index, and_imp]
intro x y a has ha b hbs hb
have h : max a b ∈ s := max_rec' _ has hbs
exact ⟨_, h, H (max a b) h (lt_max_of_lt_left ha) (lt_max_of_lt_right hb)⟩
· rwa [csSup_of_not_bddAbove hs]
