Theorems · Theorem · general topology
IsOpenMap.nhds_le
∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
IsOpenMap f → ∀ (x : X), nhds (f x) ≤ Filter.map f (nhds x)- Defined in
- Mathlib.Topology.Maps.Basic
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 61 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setproof · cited by 53,352
- TopologicalSpacestatement and proof · cited by 24,529
- Filterstatement · cited by 8,121
- nhdsstatement · cited by 5,554
- Filter.mapstatement · cited by 819
- IsOpenMapstatement and proof · cited by 253
- IsOpenMap.image_mem_nhdsproof · cited by 10
- Filter.le_mapproof · cited by 6
Cited by11
Results whose statement or proof uses this declaration.
- Topology.IsOpenEmbedding.of_continuous_injective_isOpenMapproof · cited by 13
- isOpenMap_iff_nhds_leproof · cited by 6
- IsOpenMap.prodMapproof · cited by 6
- IsOpenMap.clusterPt_comapproof · cited by 3
- IsOpenQuotientMap.map_nhds_eqproof · cited by 3
- IsTopologicalGroup.isOpenMap_iff_nhds_oneproof · cited by 1
- IsOpenMap.map_nhds_eqproof · cited by 1
- IsOpenMap.piMapproof · cited by 1
- IsDiscrete.image_of_isOpenMap_of_isOpenproof · cited by 1
- IsTopologicalAddGroup.isOpenMap_iff_nhds_zeroproof · cited by 0
- IsDiscrete.image_of_isOpenMapproof · cited by 0