English
The second projection maps nhdsWithin to nhds in the second coordinate.
Русский
Вторая проекция переводит nhdsWithin в nhds по второй координате.
LaTeX
$$$$\mathrm{map\,Prod.snd}\,(\mathcal N_{(x,y)}^{\text{within}}) = \mathcal N_y.$$$$
Lean4
/-- `Prod.snd` maps neighborhood of `x : X × Y` within the section `Prod.fst ⁻¹' {x.1}`
to `𝓝 x.2`. -/
theorem map_snd_nhdsWithin (x : X × Y) : map Prod.snd (𝓝[Prod.fst ⁻¹' { x.1 }] x) = 𝓝 x.2 :=
by
refine le_antisymm (continuousAt_snd.mono_left inf_le_left) fun s hs => ?_
rcases x with ⟨x, y⟩
rw [mem_map, nhdsWithin, mem_inf_principal, mem_nhds_prod_iff] at hs
rcases hs with ⟨u, hu, v, hv, H⟩
simp only [prod_subset_iff, mem_singleton_iff, mem_setOf_eq, mem_preimage] at H
exact mem_of_superset hv fun z hz => H _ (mem_of_mem_nhds hu) _ hz rfl
