English
Analyzes how the first projection behaves on neighbourhoods within a fiber: map fst of nhdsWithin equals nhds of the first coordinate.
Русский
Изучается поведение проекции fst на окрестности внутри волокна: образ fst от nhdsWithin равен nhds первой координаты.
LaTeX
$$$$\mathrm{map}\,\mathrm{Prod.fst}\,(\mathcal N_{x})=\mathcal N_{x.1}.$$$$
Lean4
/-- `Prod.fst` maps neighborhood of `x : X × Y` within the section `Prod.snd ⁻¹' {x.2}`
to `𝓝 x.1`. -/
theorem map_fst_nhdsWithin (x : X × Y) : map Prod.fst (𝓝[Prod.snd ⁻¹' { x.2 }] x) = 𝓝 x.1 :=
by
refine le_antisymm (continuousAt_fst.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 hu fun z hz => H _ hz _ (mem_of_mem_nhds hv) rfl
