continuousOn_iff — Mathlib

English

If g is an inducing map, then a function f is continuous on s iff g ∘ f is continuous on s.

Русский

Если g является индуциирующим отображением, то функция f непрерывна на s тогда и только тогда, когда g ∘ f непрерывна на s.

LaTeX

$$$\\text{IsInducing } g \\Rightarrow (\\text{ContinuousOn } f\\ s) \\iff (\\text{ContinuousOn } (g \\circ f)\\ s)$$$

Lean4

theorem continuousOn_iff {f : α → β} {g : β → γ} (hg : IsInducing g) {s : Set α} :
    ContinuousOn f s ↔ ContinuousOn (g ∘ f) s := by simp_rw [ContinuousOn, hg.continuousWithinAt_iff]

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