English
Let f: ι → α, i ∈ ι, and x ∈ α. Under the standing assumptions (ι preorder, LocallyFiniteOrderBot, α distributive lattice with bottom), the initial join up to i is disjoint from x if and only if every f(j) with j ≤ i is disjoint from x.
Русский
Пусть f: ι → α, i ∈ ι, и x ∈ α. При обычных предположениях (упорядочение на ι, локально конечный порядок с нулём, α — распределённая решётка с нулём) объединение значений f(j) по всем j ≤ i не пересекается с x тогда и только тогда каждый f(j) с j ≤ i не пересекается с x.
LaTeX
$$$\operatorname{Disjoint}\big(\operatorname{partialSups} f\, i, x\big) \iff \forall j \le i,\; \operatorname{Disjoint}\big(f(j), x\big)$$$
Lean4
@[simp]
theorem disjoint_partialSups_left {f : ι → α} {i : ι} {x : α} :
Disjoint (partialSups f i) x ↔ ∀ j ≤ i, Disjoint (f j) x :=
partialSups_iff_forall (Disjoint · x) disjoint_sup_left
