nontrivial_iff

Mathlib.Topology.Inseparable

URI: https://scilib.ai/kg/mathlib#SeparationQuotient.nontrivial_iff

← MathLib Explorer

English

For α with topology t, Nontrivial(SeparationQuotient α) iff t ≠ ⊤.

Русский

Для α с топологией t, Nontrivial(SeparationQuotient α) эквивално t ≠ ⊤.

LaTeX

$$$\\text{Nontrivial}(\\mathrm{SeparationQuotient}(\\alpha)) \\iff t \\neq \\top$$$

Lean4

theorem nontrivial_iff {t : TopologicalSpace α} : Nontrivial (SeparationQuotient α) ↔ t ≠ ⊤ := by
  simpa only [not_subsingleton_iff_nontrivial] using subsingleton_iff.not

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

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

Разделы

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

Аффилиация

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