Extra lemmas on WithTop

instance instIsBotOneClassWithTop_combinatorialGames {α : Type u_1} [LE α] [One α] [IsBotOneClass α] : IsBotOneClass (WithTop α)

instance instIsBotZeroClassWithTop_combinatorialGames {α : Type u_1} [LE α] [Zero α] [IsBotZeroClass α] : IsBotZeroClass (WithTop α)

@[instance_reducible]

instance instSuccAddOrderWithTopOfNoMaxOrderOfDecidableEqSucc_combinatorialGames {α : Type u_1} [PartialOrder α] [Add α] [One α] [SuccAddOrder α] [NoMaxOrder α] [(a : α) → Decidable (Order.succ a = a)] : SuccAddOrder (WithTop α)

Equations

• instSuccAddOrderWithTopOfNoMaxOrderOfDecidableEqSucc_combinatorialGames = { toSuccOrder := WithTop.instSuccOrder, succ_eq_add_one := ⋯ }

theorem WithTop.coe_add_one {α : Type u_1} [Add α] [One α] (x : α) : ↑(x + 1) = ↑x + 1

theorem small_of_image {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} (hf : Set.InjOn f s) [Small.{u, u_2} ↑(f '' s)] : Small.{u, u_1} ↑s

theorem small_image_iff {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} (hf : Set.InjOn f s) : Small.{u, u_2} ↑(f '' s) ↔ Small.{u, u_1} ↑s

theorem NatOrdinal.withTop_iSup_coe_lt {ι : Type u_1} [Small.{u, u_1} ι] (f : ι → NatOrdinal) : ⨆ (i : ι), ↑(f i) < ⊤

theorem NatOrdinal.withTop_sSup_coe_lt (s : Set NatOrdinal) [Small.{u, u + 1} ↑s] : sSup (WithTop.some '' s) < ⊤

theorem NatOrdinal.withTop_iSup_lt_top_iff_of_forall_lt {ι : Sort u_1} {f : ι → WithTop NatOrdinal} (h : ∀ (i : ι), f i < ⊤) : ⨆ (i : ι), f i < ⊤ ↔ Small.{u, u + 1} ↑(Set.range f)

theorem NatOrdinal.withTop_sSup_lt_top_iff_of_forall_lt {s : Set (WithTop NatOrdinal)} (h : ∀ x ∈ s, x < ⊤) : sSup s < ⊤ ↔ Small.{u, u + 1} ↑s

@[simp]

theorem NatOrdinal.withTop_iSup_lt_top {ι : Type u_1} [Small.{u, u_1} ι] {f : ι → WithTop NatOrdinal} : ⨆ (i : ι), f i < ⊤ ↔ ∀ (i : ι), f i < ⊤

@[simp]

theorem NatOrdinal.withTop_sSup_lt_top {s : Set (WithTop NatOrdinal)} [Small.{u, u + 1} ↑s] : sSup s < ⊤ ↔ ∀ x ∈ s, x < ⊤