semilatticeSup — Mathlib

English

For Ioi(a), a semilatticeSup structure is inherited from α with the join compatible with x > a.

Русский

Ioi(a) наследует структуру SemilatticeSup от α, сочетаемость операции ⊔ с условием x > a.

LaTeX

$$$[SemilatticeSup\\;α] {a:\\alpha} : \\mathrm{SemilatticeSup}(\\mathrm{Ioi}\\;a).Elem$$$

Lean4

instance semilatticeSup [SemilatticeSup α] {a : α} : SemilatticeSup (Ioi a) :=
  Subtype.semilatticeSup fun _ _ hx _ => lt_of_lt_of_le hx le_sup_left

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