Theorems · Theorem · general topology

comap_coe_nhdsLT_eq_atTop_iff

∀ {X : Type u_1} [inst : LinearOrder X] [inst_1 : TopologicalSpace X] [OrderTopology X] {s : Set X} {b : X},
  Filter.comap Subtype.val (nhdsWithin b (Set.Iio b)) = Filter.atTop ↔
    s ⊆ Set.Iio b ∧ (s.Nonempty → ∀ a < b, (s ∩ Set.Ioo a b).Nonempty)

Defined in: Mathlib.Topology.Order.AtTopBotIxx
Cited by: 2 results in Mathlib
Foundations: Depth 79 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: LinearOrder TopologicalSpace OrderTopology

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites33

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
TopologicalSpacestatement and proof · cited by 24,529
LinearOrderstatement and proof · cited by 8,572
Filterstatement and proof · cited by 8,121
Set.Elemproof · cited by 7,166
Set.preimageproof · cited by 4,946
Filter.Tendstoproof · cited by 3,814
Set.Nonemptystatement and proof · cited by 2,627
Filter.atTopstatement and proof · cited by 2,405
nhdsWithinstatement and proof · cited by 1,912
OrderTopologystatement and proof · cited by 1,355
Set.Ioostatement and proof · cited by 1,214

Cited by2

Results whose statement or proof uses this declaration.

comap_coe_nhdsLT_of_Ioo_subsetproof · cited by 3
comap_coe_nhdsGT_eq_atBot_iffproof · cited by 0