OrdinalIndex.lean

1import BFPP.Realization2import Mathlib.SetTheory.Ordinal.Topology3import Mathlib.Order.SuccPred.Basic45/-! # Concrete ordinal index spaces -/67namespace BFPP89set_option autoImplicit false1011open Set Order1213universe u1415abbrev OrdinalIndex (τ : Ordinal.{u}) := Set.Iio τ1617variable (τ : Ordinal.{u}) [hτ : Fact (IsSuccLimit τ)]1819instance ordinalIndexOrderBot : OrderBot (OrdinalIndex τ) where20  bot := ⟨0, hτ.out.pos⟩21  bot_le i := by22    change (0 : Ordinal.{u}) ≤ i.val23    exact bot_le2425instance ordinalIndexNoMaxOrder : NoMaxOrder (OrdinalIndex τ) :=26  hτ.out.isSuccPrelimit.noMaxOrder_Iio2728noncomputable instance ordinalIndexSuccOrder : SuccOrder (OrdinalIndex τ) :=29  SuccOrder.ofLinearWellFoundedLT _3031instance ordinalIndexCompactIcc : CompactIccSpace (OrdinalIndex τ) where32  isCompact_Icc {a b} := by33    apply Topology.IsEmbedding.subtypeVal.isCompact_iff.mpr34    have he : Subtype.val '' (Icc a b) = Icc a.val b.val := by35      ext i36      constructor37      · rintro ⟨j, hj, rfl⟩38        exact hj39      · intro hi40        exact ⟨⟨i, lt_of_le_of_lt hi.2 b.property⟩, hi, rfl⟩41    rw [he]42    exact isCompact_Icc4344example : OrderTopology (OrdinalIndex τ) := inferInstance45example : CompactIccSpace (OrdinalIndex τ) := inferInstance46example : WellFoundedLT (OrdinalIndex τ) := inferInstance4748end BFPP

SHA-256