toDistribLattice — Mathlib

English

Let α be a coframe. Then α is a distributive lattice, i.e. for all a, b, c in α, a ∧ (b ∨ c) = (a ∧ b) ∨ (a ∧ c).

Русский

Пусть α — когрейм. Тогда она является распределённой решёткой: для всех a, b, c ∈ α выполняется a ∧ (b ∨ c) = (a ∧ b) ∨ (a ∧ c).

LaTeX

$$$\forall a,b,c \in \alpha\; :\; a \wedge (b \vee c) = (a \wedge b) \vee (a \wedge c)\,.$$$

Lean4

instance (priority := 100) toDistribLattice : DistribLattice α
    where
  __ := ‹Coframe α›
  le_sup_inf a b c := by rw [← sInf_pair, ← sInf_pair, sup_sInf_eq, ← sInf_image, image_pair]

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