semilatticeInf — Mathlib

English

If α has an infimum, then Ici a inherits a semilatticeInf structure by defining x ⊓ y via the ambient infimum in α.

Русский

Если в α существует inf, то интервал вверх Ici a наследует структуру полупрещеленной инф через инф α.

LaTeX

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

Lean4

instance semilatticeInf [SemilatticeInf α] {a : α} : SemilatticeInf (Ici a) :=
  Subtype.semilatticeInf fun _ _ hx hy => le_inf hx hy

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