continuousOn_isOpen_iff — Mathlib

English

Let f be a quotient map. For any open s ⊆ β, a function g is continuous on s iff g ∘ f is continuous on f^{-1}(s).

Русский

Пусть f — квотиентное отображение. Для любого открытого s ⊆ β, функция g непрерывна на s тогда и только тогда, когда g ∘ f непрерывна на f^{-1}(s).

LaTeX

$$$\\text{IsQuotientMap } f \\Rightarrow \\forall s\\; (\\text{IsOpen } s) \\Rightarrow (\\text{ContinuousOn } g\\ s \\iff \\text{ContinuousOn } (g \\circ f) (f^{-1}' s))$$$

Lean4

theorem continuousOn_isOpen_iff {f : α → β} {g : β → γ} (h : IsQuotientMap f) {s : Set β} (hs : IsOpen s) :
    ContinuousOn g s ↔ ContinuousOn (g ∘ f) (f ⁻¹' s) :=
  by
  simp only [continuousOn_iff_continuous_restrict, (h.restrictPreimage_isOpen hs).continuous_iff]
  rfl

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