comp_continuous_iff

Mathlib.Analysis.Normed.Affine.Isometry

URI: https://scilib.ai/kg/mathlib#AffineIsometryEquiv.comp_continuous_iff

English

AffineIsometryEquiv preserves ordinary continuity of maps: Continuous(e ∘ f) iff Continuous(f).

Русский

AffineIsometryEquiv сохраняет обычную непрерывность отображений: Continuous(e ∘ f) ⇔ Continuous(f).

LaTeX

$$$\mathrm{Continuous}(e \circ f) \iff \mathrm{Continuous}(f)$$$

Lean4

@[simp]
theorem comp_continuous_iff {f : α → P} : Continuous (e ∘ f) ↔ Continuous f :=
  e.isometry.comp_continuous_iff

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru