English
From the dual distributive law, a lattice structure can be obtained to make α a distributive lattice.
Русский
Из двойственного распределительного закона можно получить структуру решётки так, чтобы α стала распределительной решёткой.
LaTeX
$$$\text{If } \forall a,b,c,\ a \wedge (b \vee c) \le a \wedge b \vee a \wedge c, \text{ then } \text{DistributiveLattice } α$$$
Lean4
/-- Prove distributivity of an existing lattice from the dual distributive law. -/
abbrev ofInfSupLe [Lattice α] (inf_sup_le : ∀ a b c : α, a ⊓ (b ⊔ c) ≤ a ⊓ b ⊔ a ⊓ c) : DistribLattice α where
le_sup_inf :=
(@OrderDual.instDistribLattice αᵒᵈ { inferInstanceAs (Lattice αᵒᵈ) with le_sup_inf := inf_sup_le }).le_sup_inf
