comp_continuousOn_iff — Mathlib

English

For an isometry f, composition with f preserves continuity on a set: ContinuousOn (f ∘ g) s iff ContinuousOn g s.

Русский

Для изометрии f композиция f ∘ g сохраняет непрерывность на заданном множестве: ContinuousOn (f ∘ g) s экв. ContinuousOn g s.

LaTeX

$$$ContinuousOn (f \circ g)\ s \iff ContinuousOn g\ s$$$

Lean4

theorem comp_continuousOn_iff {γ} [TopologicalSpace γ] (hf : Isometry f) {g : γ → α} {s : Set γ} :
    ContinuousOn (f ∘ g) s ↔ ContinuousOn g s :=
  hf.isUniformInducing.isInducing.continuousOn_iff.symm

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