t1Space_antitone

Mathlib.Topology.Separation.Basic

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

English

The assignment X ↦ T1Space X is antitone with respect to refinement of topologies.

Русский

Присвоение X ↦ T1Space X антотонно по отношению к уточнению топологий.

LaTeX

$$Antitone(T1Space) holds: if X ≤ Y then T1Space X ≤ T1Space Y.$$

Lean4

theorem t1Space_antitone {X} : Antitone (@T1Space X) := fun a _ h _ => @T1Space.mk _ a fun x => (T1Space.t1 x).mono h

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

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

Разделы

Аффилиация

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