continuousWithinAt_iff_continuousWithinAt_comp_right

English

Continuity at a point is preserved under right composition with an open partial homeomorphism: if x ∈ target, then ContinuousAt f x iff ContinuousAt (f ∘ e) (e.symm x).

Русский

Непрерывность в точке сохраняется при правой композиции с открытым частичным гомеоморфизмом: если x принадлежит target, то ContinuousAt f x эквивалично ContinuousAt (f ∘ e) (e.symm x).

LaTeX

$$$\forall f, s, x, (x \in e.target) \Rightarrow (ContinuousAt\ f\ x \iff\ ContinuousAt\ (f \circ e)\ (e.symm x))$$$

Lean4

/-- Continuity within a set at a point can be read under right composition with a local
homeomorphism, if the point is in its target -/
theorem continuousWithinAt_iff_continuousWithinAt_comp_right {f : Y → Z} {s : Set Y} {x : Y} (h : x ∈ e.target) :
    ContinuousWithinAt f s x ↔ ContinuousWithinAt (f ∘ e) (e ⁻¹' s) (e.symm x) := by
  simp_rw [ContinuousWithinAt, ← @tendsto_map'_iff _ _ _ _ e, e.map_nhdsWithin_preimage_eq (e.map_target h), (· ∘ ·),
    e.right_inv h]

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