instDistribLattice — Mathlib

English

The complemented elements form a distributive lattice, inherited from α via the coercion, with lattice operations defined coordinatewise.

Русский

Дополненные элементы образуют распределённую решётку, которая наследуется от α через вложение, причём операции ∨, ∧ выполняются по координатам.

LaTeX

$$$\mathrm{Complementeds}(\alpha) \text{ is a DistribLattice, obtained from } \alpha \text{ via } a \lor b, a \land b \text{ with } \mathrm{val} \text{ preserved by } \mathrm{coe\_sup}, \mathrm{coe\_inf}.$$$

Lean4

instance : DistribLattice (Complementeds α) :=
  Complementeds.coe_injective.distribLattice _ coe_sup coe_inf

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