partialOrder — Mathlib

English

The open neighborhood system OpenNhds x carries a lattice structure under inclusion, with inf being intersection and sup being union, compatible with the ambient topology.

Русский

Система открытых окрестностей OpenNhds x образует решётку относительно включения: наибольшая общая часть — пересечение, наименьшая — объединение, совместимо с топологией окружающего пространства.

LaTeX

$$$\\text{OpenNhds}(x)$ is a lattice under inclusion, with $U \\wedge V = U\\cap V$ and $U \\vee V = U \\cup V$.$$

Lean4

instance partialOrder (x : X) : PartialOrder (OpenNhds x)
    where
  le U V := U.1 ≤ V.1
  le_refl _ := le_rfl
  le_trans _ _ _ := le_trans
  le_antisymm _ _ i j := ObjectProperty.FullSubcategory.ext <| le_antisymm i j

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