instLatticeElem — Mathlib

English

If α is a lattice and a ∈ α, the lower interval Iic(a) = { x ∈ α | x ≤ a } carries a lattice structure under the inherited order, with the meet and join operations on Iic(a) given by the ambient inf and sup restricted to Iic(a).

Русский

Пусть α — решётка и a ∈ α. Тогда нижний интервал Iic(a) = { x ∈ α | x ≤ a } образует решётку под унаследованным порядком; операции meet и join на Iic(a) задаются ограничениями от α.

LaTeX

$$$$\\forall x,y \\in \\mathrm{Iic}(a),\\; x \\wedge_{\\mathrm{Iic}(a)} y = x \\wedge_\\alpha y,\\quad x \\vee_{\\mathrm{Iic}(a)} y = x \\vee_\\alpha y.$$$$

Lean4

instance [Lattice α] : Lattice (Iic a) :=
  { Iic.semilatticeInf, Iic.semilatticeSup with }

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