instT0Space

Mathlib.Topology.EMetricSpace.Basic

URI: https://scilib.ai/kg/mathlib#EMetricSpace.instT0Space

English

An emetric space is a T0 space.

Русский

Эметрическое пространство является T0-пространством.

LaTeX

$$T0Space γ$$

Lean4

/-- An emetric space is separated -/
instance (priority := 100) instT0Space : T0Space γ where t0 _ _ h := eq_of_edist_eq_zero <| inseparable_iff.1 h

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

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

Разделы

Аффилиация

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