instMinOfT2Space

Mathlib.Topology.Sets.Compacts

URI: https://scilib.ai/kg/mathlib#TopologicalSpace.Compacts.instMinOfT2Space

English

The minimal operation on compact subsets is intersection: the minimum is s ∩ t, which is compact if s and t are compact.

Русский

Минимумом по компактах является пересечение: s ∩ t компактно, если s и t компактны.

LaTeX

$$$s \min t = s \cap t$ with $s,t$ compact.$$

Lean4

instance [T2Space α] : Min (Compacts α) :=
  ⟨fun s t => ⟨s ∩ t, s.isCompact.inter t.isCompact⟩⟩

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

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

Разделы

Аффилиация

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