Theorems · Theorem · general topology
map_snd_nhdsWithin
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (x : X × Y),
Filter.map Prod.snd (nhdsWithin x (Prod.fst ⁻¹' {x.1})) = nhds x.2Prod.snd maps neighborhood of x : X × Y within the section Prod.fst ⁻¹' {x.1}
to 𝓝 x.2.
- Defined in
- Mathlib.Topology.Constructions.SumProd
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites18
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
- Filterstatement and proof · cited by 8,121
- Set.ofPredproof · cited by 6,101
- nhdsstatement and proof · cited by 5,554
- Set.preimagestatement and proof · cited by 4,946
- le_antisymmproof · cited by 2,068
- nhdsWithinstatement and proof · cited by 1,912
- SProd.sprodproof · cited by 1,750
- Filter.mapstatement and proof · cited by 819
- Filter.mem_of_supersetproof · cited by 308
- inf_le_leftproof · cited by 286
Cited by2
Results whose statement or proof uses this declaration.
- IsLocalExtrOn.range_ne_top_of_hasStrictFDerivAtproof · cited by 1
- map_snd_nhdsproof · cited by 1