English
Let f be a function from the disjoint sum α ⊕ β to ordinals. Then the supremum of f is the maximum of the supremums taken over the left and right injections.
Русский
Пусть f: α ⊕ β → Ordinal. Тогда супремум f равен максимуму из супремумов по левой и правой частью через внедрения inl и inr.
LaTeX
$$$$ \\mathrm{iSup}\tfrac{f}{ } = \\max\\Big( \\mathrm{iSup}\\big( a \\mapsto f(\\mathrm{Sum}.inl\,a) \\big), \\mathrm{iSup}\\big( b \\mapsto f(\\mathrm{Sum}.inr\,b) \\big) \\Big) $$$$
Lean4
theorem iSup_sum {α β} (f : α ⊕ β → Ordinal.{u}) [Small.{u} α] [Small.{u} β] :
iSup f = max (⨆ a, f (Sum.inl a)) (⨆ b, f (Sum.inr b)) :=
by
apply (Ordinal.iSup_le _).antisymm (max_le _ _)
· rintro (i | i)
· exact le_max_of_le_left (Ordinal.le_iSup (fun x ↦ f (Sum.inl x)) i)
· exact le_max_of_le_right (Ordinal.le_iSup (fun x ↦ f (Sum.inr x)) i)
all_goals
apply csSup_le_csSup' (bddAbove_of_small _)
rintro i ⟨a, rfl⟩
apply mem_range_self
