semilatticeInf — Mathlib

English

For any a < b, the interval Ico(a,b) inherits a semilatticeInf structure from the ambient semilattice via the operation defined pointwise.

Русский

Для любой пары a < b интервал Ico(a,b) наследует структуру полусоединенного инфмуля через операцию meet, взятую по элементам Ambient.

LaTeX

$$$[SemilatticeInf\\;α] {a\\,b:\\alpha} :\\mathrm{SemilatticeInf}(\\mathrm{Ico}\\;a\\;b)$$$

Lean4

instance semilatticeInf [SemilatticeInf α] {a b : α} : SemilatticeInf (Ico a b) :=
  Subtype.semilatticeInf fun _ _ hx hy => ⟨le_inf hx.1 hy.1, lt_of_le_of_lt inf_le_left hx.2⟩

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