Theorems · Theorem · general topology

map_coe_atTop_of_Ioo_subset

∀ {X : Type u_1} [inst : LinearOrder X] [inst_1 : TopologicalSpace X] [OrderTopology X] {s : Set X} {b : X},
  s ⊆ Set.Iio b →
    (∀ a' < b, ∃ a < b, Set.Ioo a b ⊆ s) →
      autoParam (Order.IsSuccPrelimit b) map_coe_atTop_of_Ioo_subset._auto_1 →
        Filter.map Subtype.val Filter.atTop = nhdsWithin b (Set.Iio b)

Defined in

Mathlib.Topology.Order.AtTopBotIxx

Cited by

2 results in Mathlib

Foundations

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

Assumes

LinearOrderTopologicalSpaceOrderTopology