instMax

Mathlib.Topology.Sets.Opens

URI: https://scilib.ai/kg/mathlib#TopologicalSpace.OpenNhdsOf.instMax

English

The join (least upper bound) of two open neighborhoods is their union.

Русский

Слияние (наименьшая верхняя граница) двух открытых окрестностей есть их объединение.

LaTeX

$$$\\\\forall U V : \\\\mathrm{OpenNhdsOf}(x),\\\\ (U \\\\lor V) = (U.1 \\\\cup V.1, Or.inl U.2).$$$

Lean4

instance : Max (OpenNhdsOf x) :=
  ⟨fun U V => ⟨U.1 ⊔ V.1, Or.inl U.2⟩⟩

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

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

Разделы

Аффилиация

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