instSemilatticeSup — Mathlib

English

If β is a lattice, then Germ l β is a lattice, having both sup and inf defined coordinatewise by the corresponding operations on β.

Русский

Если β — решётка, то Germ l β тоже является решёткой, где верх и низ определяются по координатам через соответствующие операции β.

LaTeX

$$$\\text{Lattice}(\\mathrm{Germ}_l \\beta)$$$

Lean4

instance instSemilatticeSup [SemilatticeSup β] : SemilatticeSup (Germ l β)
    where
  sup := max
  le_sup_left f g := inductionOn₂ f g fun _f _g => Eventually.of_forall fun _x ↦ le_sup_left
  le_sup_right f g := inductionOn₂ f g fun _f _g ↦ Eventually.of_forall fun _x ↦ le_sup_right
  sup_le f₁ f₂ g := inductionOn₃ f₁ f₂ g fun _f₁ _f₂ _g h₁ h₂ ↦ h₂.mp <| h₁.mono fun _x ↦ sup_le

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