Club sets

A subset of a well-ordered type α is called a club set when it is closed in the order topology and cofinal. If α has no maximum, then an equivalent condition is that α is closed and unbounded; hence the name.

Implementation notes

To avoid importing topology in the ordinals, we spell out the closure property using DirSupClosed. For any type equipped with the Scott-Hausdorff topology (which includes well-orders with the order topology), DirSupClosed s and IsClosed s are equivalent predicates.

structure IsClub {α : Type u_1} [LinearOrder α] (s : Set α) : Prop

A club set is closed under suprema and cofinal.

• dirSupClosed : DirSupClosed s

  Club sets are closed under suprema. If α is a well-order with the order topology, this condition is equivalent to IsClosed s.

• isCofinal : IsCofinal s

  Club sets are cofinal. If α has no maximum, this condition is equivalent to ¬ BddAbove s. See not_bddAbove_iff_isCofinal.

@[simp]

theorem IsClub.of_isEmpty {α : Type v} [LinearOrder α] [IsEmpty α] {s : Set α} : IsClub s

@[simp]

theorem IsClub.univ {α : Type v} [LinearOrder α] : IsClub Set.univ

theorem IsClub.union {α : Type v} {s t : Set α} [LinearOrder α] (hs : IsClub s) (ht : IsClub t) : IsClub (s ∪ t)

theorem IsClub.isLUB_mem {α : Type v} {s t : Set α} {x : α} [LinearOrder α] (hs : IsClub s) (ht : t ⊆ s) (ht₀ : t.Nonempty) (hx : IsLUB t x) : x ∈ s

theorem IsClub.csSup_mem {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s t : Set α} (hs : IsClub s) (ht : t ⊆ s) (ht₀ : t.Nonempty) (ht₁ : BddAbove t) : sSup t ∈ s

theorem IsClub.sInter_of_orderTop {α : Type v} [LinearOrder α] {s : Set (Set α)} [OrderTop α] (hs : ∀ x ∈ s, IsClub x) : IsClub (⋂₀ s)

theorem IsClub.iInter_of_orderTop {α : Type v} [LinearOrder α] {ι : Type u_1} {f : ι → Set α} [OrderTop α] (hs : ∀ (i : ι), IsClub (f i)) : IsClub (⋂ (i : ι), f i)

theorem IsClub.sInter_of_cof_le_one {α : Type v} [LinearOrder α] {s : Set (Set α)} (hα : Order.cof α ≤ 1) (hs : ∀ x ∈ s, IsClub x) : IsClub (⋂₀ s)

theorem IsClub.iInter_of_cof_le_one {α : Type v} [LinearOrder α] {ι : Type u_1} {f : ι → Set α} (hα : Order.cof α ≤ 1) (hs : ∀ (i : ι), IsClub (f i)) : IsClub (⋂ (i : ι), f i)

theorem IsClub.sInter {α : Type v} [LinearOrder α] [WellFoundedLT α] {s : Set (Set α)} (hα : Order.cof α ≠ Cardinal.aleph0) (hsα : Cardinal.mk ↑s < Order.cof α) (hs : ∀ x ∈ s, IsClub x) : IsClub (⋂₀ s)

theorem IsClub.iInter {α : Type v} [LinearOrder α] [WellFoundedLT α] {ι : Type u} {f : ι → Set α} (hα : Order.cof α ≠ Cardinal.aleph0) (hι : Cardinal.lift.{v, u} (Cardinal.mk ι) < Cardinal.lift.{u, v} (Order.cof α)) (hf : ∀ (i : ι), IsClub (f i)) : IsClub (⋂ (i : ι), f i)

theorem IsClub.inter {α : Type v} [LinearOrder α] [WellFoundedLT α] {s t : Set α} (hα : Order.cof α ≠ Cardinal.aleph0) (hs : IsClub s) (ht : IsClub t) : IsClub (s ∩ t)

theorem Order.IsNormal.isClub_range {α : Type v} [LinearOrder α] [WellFoundedLT α] {f : α → α} (hf : IsNormal f) : IsClub (Set.range f)

theorem Order.IsNormal.isClub_fixedPoints {α : Type v} [LinearOrder α] [WellFoundedLT α] {f : α → α} (hα : cof α ≠ Cardinal.aleph0) (hf : IsNormal f) : IsClub (Function.fixedPoints f)