instDistribLattice — Mathlib

English

The lattice operations on Germ l β are compatible with those on β: the order and lattice relations hold coordinatewise, mirroring β.

Русский

Операции решётки на Germ l β совместимы с операциями β: порядок и свойства решётки сохраняются по координатам.

LaTeX

$$$(\\mathrm{Germ}_l \\beta)$ satisfies the lattice axioms with pointwise definitions of $\\sup$ and $\\inf$$$

Lean4

instance instDistribLattice [DistribLattice β] : DistribLattice (Germ l β) where
  le_sup_inf f g h := inductionOn₃ f g h fun _f _g _h ↦ Eventually.of_forall fun _ ↦ le_sup_inf

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