Theorems · Theorem · logic and foundations

Ordinal.iSup_sum

∀ {α : Type u_3} {β : Type u_4} (f : α ⊕ β → Ordinal.{u}) [Small.{u, u_3} α] [Small.{u, u_4} β],
  iSup f = max (⨆ a, f (Sum.inl a)) (⨆ b, f (Sum.inr b))

Defined in

Mathlib.SetTheory.Ordinal.Family

Cited by

1 results in Mathlib

Foundations

Depth 83 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SmallSmall