English
Let α be a distributive lattice and s, t, u finite subsets of α. Then the set of all infima a ∧ (b ∨ c) with a ∈ s, b ∈ t, c ∈ u and Disjoint(b, c) is contained in the set of all (a ∧ b) ∨ (a ∧ c) with a ∈ s, b ∈ t, c ∈ u. In symbols: s ⊼ (t ⊻ u) ⊆ s ⊼ t ⊻ s ⊼ u.
Русский
Пусть α — распределительная решётка, и s, t, u — конечные подмножества α. Тогда множество элементов вида a ∧ (b ∨ c) с a ∈ s, b ∈ t, c ∈ u и Disjoint(b, c) содержится в множестве элементов (a ∧ b) ∨ (a ∧ c) с a ∈ s, b ∈ t, c ∈ u. В явном виде: s ⊼ (t ⊻ u) ⊆ s ⊼ t ⊻ s ⊼ u.
LaTeX
$$$ s \wedge \bigl(t \vee u\bigr) \subseteq \bigl(s \wedge t\bigr) \vee \bigl(s \wedge u\bigr) $$$
Lean4
theorem infs_sups_subset_left : s ⊼ (t ⊻ u) ⊆ s ⊼ t ⊻ s ⊼ u :=
image₂_distrib_subset_left inf_sup_left
