comp_continuous_iff — Mathlib

English

If f is a linear isometry, then composing with f preserves continuity: Continuous(f ∘ g) is equivalent to Continuous(g).

Русский

Если f является линейной изометрией, то композиция c f сохраняет непрерывность: непрерывность f ∘ g эквивалентна непрерывности g.

LaTeX

$$Continuous (f ∘ g) ⇔ Continuous g$$

Lean4

@[simp]
theorem comp_continuous_iff {α : Type*} [TopologicalSpace α] {g : α → E} : Continuous (f ∘ g) ↔ Continuous g :=
  f.isometry.comp_continuous_iff

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