stableUnderSpecialization

Mathlib.Topology.Inseparable

URI: https://scilib.ai/kg/mathlib#IsClosed.stableUnderSpecialization

English

If s is closed, then s is stable under specialization.

Русский

Если s замкнуто, то оно стабильно по специализации.

LaTeX

$$$$ IsClosed(s) \rightarrow StableUnderSpecialization(s). $$$$

Lean4

theorem stableUnderSpecialization {s : Set X} (hs : IsClosed s) : StableUnderSpecialization s := fun _ _ e ↦
  e.mem_closed hs

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

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

Разделы

Аффилиация

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