Theorems · Theorem · general topology
Topology.IsOpenEmbedding.map_nhds_eq
∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
Topology.IsOpenEmbedding f → ∀ (x : X), Filter.map f (nhds x) = nhds (f x)- Defined in
- Mathlib.Topology.Maps.Basic
- Cited by
- 22 results in Mathlib
- Foundations
- Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement and proof · cited by 24,529
- Filterstatement · cited by 8,121
- nhdsstatement · cited by 5,554
- Filter.mapstatement · cited by 819
- IsOpen.mem_nhdsproof · cited by 470
- Set.mem_range_selfproof · cited by 328
- Topology.IsOpenEmbeddingstatement and proof · cited by 231
- Topology.IsOpenEmbedding.isOpen_rangeproof · cited by 33
- Topology.IsOpenEmbedding.isEmbeddingproof · cited by 22
- Topology.IsEmbedding.map_nhds_of_memproof · cited by 2
Cited by22
Results whose statement or proof uses this declaration.
- RestrictedProduct.nhds_eq_map_inclusionproof · cited by 5
- Topology.IsOpenEmbedding.image_mem_nhdsproof · cited by 4
- Topology.IsOpenEmbedding.isOpenMap_iffproof · cited by 4
- ENNReal.nhds_coeproof · cited by 3
- Sigma.nhds_mkproof · cited by 3
- UpperHalfPlane.hasStrictDerivAt_smulproof · cited by 3
- ENNReal.nhds_coe_coeproof · cited by 2
- OnePoint.nhds_coe_eqproof · cited by 2
- UpperHalfPlane.eq_zero_of_frequentlyproof · cited by 2
- nhds_inlproof · cited by 2
- nhds_inrproof · cited by 2
- Topology.IsOpenEmbedding.tendsto_nhds_iff'proof · cited by 1