Theorems · Theorem · logic and foundations

IsClub.isNormal_enum

∀ {α : Type v} [inst : LinearOrder α] [inst_1 : WellFoundedLT α] [inst_2 : IsRegularCardinalOrder α] {s : Set α}
  (hs : IsClub s), Order.IsNormal (Subtype.val ∘ ⇑(Order.enum s ⋯))

Defined in

Mathlib.SetTheory.Cardinal.Cofinality.Club

Cited by

0 results in Mathlib

Foundations

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

Assumes

LinearOrderWellFoundedLTIsRegularCardinalOrder