t1Space_iff_t0Space_and_r0Space

Mathlib.Topology.Separation.Basic

URI: https://scilib.ai/kg/mathlib#t1Space_iff_t0Space_and_r0Space

English

A T1 space is equivalent to the conjunction of T0 and R0 spaces.

Русский

T1-пространство эквивалентно сочетанию T0 и R0 пространств.

LaTeX

$$$T1Space(X) \\iff (T0Space(X) \\land R0Space(X)).$$$

Lean4

theorem t1Space_iff_t0Space_and_r0Space : T1Space X ↔ T0Space X ∧ R0Space X :=
  (t1Space_TFAE X).out 0 10

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

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

Разделы

Аффилиация

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