English
If α and β are distributive lattices, then their Lex sum α ⊕ₗ β is a distributive lattice, with the distributive law holding with respect to the Lex-defined sup and inf.
Русский
Если α и β — распределительные решетки, то их лексикографическая сумма α ⊕ₗ β является распределительной решеткой; закон распределения выполняется относительно операций ⊔ и ⊓, определённых по Lex.
LaTeX
$$$\\text{instDistribLattice } (\\alpha,\\beta): \\text{DistribLattice}(\\mathrm{Lex}(\\alpha,\\beta))$ with axioms $a\\le\\, (b\\sqcup c)$ imply etc.$$
Lean4
instance instDistribLattice [DistribLattice α] [DistribLattice β] : DistribLattice (α ⊕ₗ β) where
le_sup_inf := by
simp only [Lex.forall, Sum.forall, inr_le_inr_iff, le_sup_left, inl_le_inr, sup_of_le_right, and_self,
inf_of_le_left, implies_true, inf_of_le_right, sup_of_le_left, ← inl_sup, ← inr_sup, ← inl_inf, ← inr_inf,
sup_inf_left, le_rfl]
