continuousAt_of_comp_right — Mathlib

English

Applying the base product homomorphism to a source element yields the pair.

Русский

Применение гомеоморфа произведения к элементу источника даёт пару.

LaTeX

$$$ (sourceHomeomorphBaseSetProd e) p = (\langle proj p, e.mem_source.2 \rangle, (e p).2) $$$

Lean4

/-- Read off the continuity of a function `f : Z → X` at `z : Z` by transferring via a
trivialization of `Z` containing `z`. -/
theorem continuousAt_of_comp_right {X : Type*} [TopologicalSpace X] {f : Z → X} {z : Z} (e : Trivialization F proj)
    (he : proj z ∈ e.baseSet) (hf : ContinuousAt (f ∘ e.toPartialEquiv.symm) (e z)) : ContinuousAt f z :=
  by
  have hez : z ∈ e.toPartialEquiv.symm.target :=
    by
    rw [PartialEquiv.symm_target, e.mem_source]
    exact he
  rwa [e.toOpenPartialHomeomorph.symm.continuousAt_iff_continuousAt_comp_right hez, OpenPartialHomeomorph.symm_symm]

Похожие утверждения