comp_continuousOn_iff — Mathlib

English

For h an isometry equivalence, ContinuousOn(h ∘ f) on s is equivalent to ContinuousOn f on s.

Русский

Для изометрического эквивалента h выполнено: ContinuousOn(h ∘ f) на s эквивалентно ContinuousOn f на s.

LaTeX

$$$\operatorname{ContinuousOn}(h \circ f, s) \iff \operatorname{ContinuousOn}(f, s)$$$

Lean4

@[simp]
theorem comp_continuousOn_iff {γ} [TopologicalSpace γ] (h : α ≃ᵢ β) {f : γ → α} {s : Set γ} :
    ContinuousOn (h ∘ f) s ↔ ContinuousOn f s :=
  h.toHomeomorph.comp_continuousOn_iff _ _

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