comp_continuous_iff'

Mathlib.Topology.Algebra.Algebra.Equiv

URI: https://scilib.ai/kg/mathlib#ContinuousAlgEquiv.comp_continuous_iff'

← MathLib Explorer

English

For any β, Continuous (g ∘ e) ↔ Continuous g; a prime variant.

Русский

Для любого β, Continuous (g ∘ e) ↔ Continuous g; прайм-вариант.

LaTeX

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

Lean4

theorem comp_continuous_iff' {β : Type*} [TopologicalSpace β] (e : A ≃A[R] B) {g : B → β} :
    Continuous (g ∘ e) ↔ Continuous g :=
  e.toHomeomorph.comp_continuous_iff'

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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