continuousAt

Mathlib.Topology.Algebra.Algebra.Equiv

URI: https://scilib.ai/kg/mathlib#ContinuousAlgEquiv.continuousAt

English

Composing with e preserves continuity: Continuous (e ∘ f) iff Continuous f.

Русский

Сочетание с e сохраняет непрерывность: Continuous (e ∘ f) эквивалентно Continuous f.

LaTeX

$$$ Continuous (e \circ f) \iff Continuous f $$$

Lean4

theorem continuousAt (e : A ≃A[R] B) {a : A} : ContinuousAt e a :=
  e.continuous.continuousAt

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

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

Разделы

Аффилиация

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