distribLattice — Mathlib

English

If α is a DistribLattice, then the upper set { x ∈ α : a ≤ x } with the inherited order is a DistribLattice.

Русский

Если α — дистрибьютная решётка, то верхнее множество { x ∈ α : a ≤ x } образует дистрибьютную решётку по унаследованной сортировке.

LaTeX

$$$\\forall x,y,z \\in \\alpha,\\ a \\le x,\\ a \\le y,\\ a \\le z \\Rightarrow (x \\lor y) \\land z = (x \\land z) \\lor (y \\land z)$$$

Lean4

instance distribLattice [DistribLattice α] {a : α} : DistribLattice { x : α // a ≤ x } :=
  Set.Ici.distribLattice

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