English
A technical lemma: near e(x), the preimage of s under e.symm equals the intersection with the target and a neighborhood around f(x).
Русский
Техническая лемма: около e(x) множество e.symm⁻¹'(s) совпадает с пересечением цели и окрестности вокруг f(x).
LaTeX
$$$ e.symm \\⁻¹' s =ᶠ[\\mathcal{N}(e(x))] (e.target \\cap e.symm^{-1}(s \\cap f^{-1}(t))) $$$
Lean4
/-- This lemma is useful in the manifold library in the case that `e` is a chart. It states that
locally around `e x` the set `e.symm ⁻¹' s` is the same as the set intersected with the target
of `e` and some other neighborhood of `f x` (which will be the source of a chart on `Z`). -/
theorem preimage_eventuallyEq_target_inter_preimage_inter {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Z}
{x : X} {f : X → Z} (hf : ContinuousWithinAt f s x) (hxe : x ∈ e.source) (ht : t ∈ 𝓝 (f x)) :
e.symm ⁻¹' s =ᶠ[𝓝 (e x)] (e.target ∩ e.symm ⁻¹' (s ∩ f ⁻¹' t) : Set Y) :=
by
rw [eventuallyEq_set, e.eventually_nhds _ hxe]
filter_upwards [e.open_source.mem_nhds hxe, mem_nhdsWithin_iff_eventually.mp (hf.preimage_mem_nhdsWithin ht)]
intro y hy hyu
simp_rw [mem_inter_iff, mem_preimage, mem_inter_iff, e.mapsTo hy, true_and, iff_self_and, e.left_inv hy,
iff_true_intro hyu]
