continuousOn_iff — Mathlib

English

If g is an embedding, then f is continuous on s iff g ∘ f is continuous on s.

Русский

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

LaTeX

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

Lean4

theorem continuousOn_iff {f : α → β} {g : β → γ} (hg : IsEmbedding g) {s : Set α} :
    ContinuousOn f s ↔ ContinuousOn (g ∘ f) s :=
  hg.isInducing.continuousOn_iff

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