continuousAt_iff_continuousAt_comp_right

English

A function is continuous on a set iff its right-composition with an open partial homeomorphism is continuous on the corresponding set, provided the subset is suitably mapped.

Русский

Функция непрерывна на множестве тогда и только тогда, когда её правая композиция с открытым частичным гомеоморфизмом непрерывна на соответствующем множестве при условии корректного отображения.

LaTeX

$$$\forall f\ s, (h: s \subseteq e.target) : ContinuousOn f s \iff ContinuousOn (f \circ e) (e.source \cap e^{-1}' s)$$$

Lean4

/-- Continuity at a point can be read under right composition with an open partial homeomorphism, if
the point is in its target -/
theorem continuousAt_iff_continuousAt_comp_right {f : Y → Z} {x : Y} (h : x ∈ e.target) :
    ContinuousAt f x ↔ ContinuousAt (f ∘ e) (e.symm x) := by
  rw [← continuousWithinAt_univ, e.continuousWithinAt_iff_continuousWithinAt_comp_right h, preimage_univ,
    continuousWithinAt_univ]

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