continuousOn_iff_continuousOn_comp_left

English

A function is continuous on a set iff its left-composition with an open partial homeomorphism is continuous on the corresponding set.

Русский

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

LaTeX

$$$\forall f\ s,\ h: s \subseteq f^{-1}(e.source) \Rightarrow ContinuousOn f s \iff ContinuousOn (e ∘ f) s$$$

Lean4

/-- A function is continuous on a set if and only if its composition with an open partial
homeomorphism on the left is continuous on the corresponding set. -/
theorem continuousOn_iff_continuousOn_comp_left {f : Z → X} {s : Set Z} (h : s ⊆ f ⁻¹' e.source) :
    ContinuousOn f s ↔ ContinuousOn (e ∘ f) s :=
  forall₂_congr fun _x hx =>
    e.continuousWithinAt_iff_continuousWithinAt_comp_left (h hx) (mem_of_superset self_mem_nhdsWithin h)

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