Theorems · Theorem · general topology
Topology.IsInducing.nhds_eq_comap
∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace Y] [inst_1 : TopologicalSpace X],
Topology.IsInducing f → ∀ (x : X), nhds x = Filter.comap f (nhds (f x))- Defined in
- Mathlib.Topology.Maps.Basic
- Cited by
- 39 results in Mathlib
- Foundations
- Depth 71 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
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.comapstatement · cited by 546
- Topology.IsInducingstatement and proof · cited by 266
- Topology.isInducing_iff_nhdsproof · cited by 14
Cited by39
Results whose statement or proof uses this declaration.
- Topology.IsInducing.tendsto_nhds_iffproof · cited by 15
- IsDenseInducing.nhds_eq_comapproof · cited by 7
- Topology.IsInducing.prodMapproof · cited by 7
- isComplete_image_iffproof · cited by 5
- UniformConvergenceCLM.hasBasis_nhds_zero_of_basisproof · cited by 5
- Homeomorph.nhds_eq_comapproof · cited by 4
- Topology.IsInducing.locallyCompactSpaceproof · cited by 4
- Topology.IsInducing.mapClusterPt_iffproof · cited by 4
- Topology.IsInducing.map_nhdsWithin_eqproof · cited by 4
- Topology.IsInducing.regularSpaceproof · cited by 4
- IsDenseEmbedding.subtypeproof · cited by 3
- ContinuousLinearMap.isThetaTVS_compproof · cited by 3