English
Symmetric application to a pair in the base product yields the source element.
Русский
Симметрическое применение к паре из базового множества даёт элемент источника.
LaTeX
$$$ (e.sourceHomeomorphBaseSetProd.symm p) = \langle e.symm (p.1, p.2), (sourceHomeomorphBaseSetProd_symm_apply.aux e p).2 \rangle $$$
Lean4
/-- Read off the continuity of a function `f : X → Z` at `x : X` by transferring via a
trivialization of `Z` containing `f x`. -/
theorem continuousAt_of_comp_left {X : Type*} [TopologicalSpace X] {f : X → Z} {x : X} (e : Trivialization F proj)
(hf_proj : ContinuousAt (proj ∘ f) x) (he : proj (f x) ∈ e.baseSet) (hf : ContinuousAt (e ∘ f) x) :
ContinuousAt f x := by
rw [e.continuousAt_iff_continuousAt_comp_left]
· exact hf
rw [e.source_eq, ← preimage_comp]
exact hf_proj.preimage_mem_nhds (e.open_baseSet.mem_nhds he)
