instInf — Mathlib

English

The infimum of two sublattices is their intersection, i.e., L ∧ M corresponds to L ∩ M.

Русский

Нижняя граница двух подрешеток есть их пересечение.

LaTeX

$$$ Min (Sublattice\\,\\alpha)\\,\\text{min}(L,M) = \\{\\text{carrier}=L \\cap M,\\; \\text{supClosed'}=L.supClosed\\cap M.supClosed,\\; \\text{infClosed'}=L.infClosed\\cap M.infClosed\\}$$$

Lean4

/-- The inf of two sublattices is their intersection. -/
instance instInf : Min (Sublattice α) where
  min L
    M :=
    { carrier := L ∩ M
      supClosed' := L.supClosed.inter M.supClosed
      infClosed' := L.infClosed.inter M.infClosed }

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