continuous_iff_continuous_comp_left

English

A function is continuous iff its composition with an OpenPartialHomeomorph on the left is continuous, with a corresponding equivalence when the source is univ.

Русский

Функция непрерывна тогда и только тогда, когда её композиция слева с OpenPartialHomeomorph непрерывна; в случае источника univ имеет место эквивалентность.

LaTeX

$$$\forall e: OpenPartialHomeomorph X Y, \; (h: f^{-1}' e.source = univ) \Rightarrow Continuous f \iff Continuous (e ∘ f)$$$

Lean4

/-- A function is continuous if and only if its composition with an open partial homeomorphism
on the left is continuous and its image is contained in the source. -/
theorem continuous_iff_continuous_comp_left {f : Z → X} (h : f ⁻¹' e.source = univ) :
    Continuous f ↔ Continuous (e ∘ f) := by
  simp only [← continuousOn_univ]
  exact e.continuousOn_iff_continuousOn_comp_left (Eq.symm h).subset

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