English
Let α be a distributive lattice with a top element. For any function f from an index set ι to α, and any finite subset s of ι, the codisjointness of a with the infimum of {f(i) : i ∈ s} is equivalent to the codisjointness of a with each f(i) for all i in s.
Русский
Пусть α — распределительный полупространство с верхним элементом. Для любой функции f: ι → α и любого конечного подмножества s ⊆ ι, отношение кодиссоединённости между a и инфимумом множества {f(i) : i ∈ s} эквивалентно кодиссоединённости a с каждым элементом f(i) при i ∈ s.
LaTeX
$$$\mathrm{Codisjoint}(s \inf f)\ a \iff \forall i \in s,\ \mathrm{Codisjoint}(f(i))\ a$$$
Lean4
protected theorem codisjoint_inf_left : Codisjoint (s.inf f) a ↔ ∀ ⦃i⦄, i ∈ s → Codisjoint (f i) a :=
@Finset.disjoint_sup_left αᵒᵈ _ _ _ _ _ _
