instMin

Mathlib.Topology.Sets.Opens

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

English

The meet (greatest lower bound) of two open neighborhoods is their intersection.

Русский

Встреча (первая нижняя граница) двух открытых окрестностей есть их пересечение.

LaTeX

$$$\\\\forall U V : \\\\mathrm{OpenNhdsOf}(x),\\\\ (U \\\\land V) = (U.1 \\\\cap V.1, U.2, V.2).$$$

Lean4

instance : Min (OpenNhdsOf x) :=
  ⟨fun U V => ⟨U.1 ⊓ V.1, U.2, V.2⟩⟩

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

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

Разделы

Аффилиация

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