partialSups_disjoint_of_disjoint — Mathlib

English

If the family {f(i)} is pairwise disjoint, then for any i < j, the initial join up to i is disjoint from f(j).

Русский

Если множество объектов {f(i)} попарно непересекается, то при любых i < j начальное объединение до i непересекается с f(j).

LaTeX

$$$\text{If } h: \text{Pairwise (Disjoint on } f) \text{ and } i < j, \\; \operatorname{Disjoint}(\operatorname{partialSups} f\, i, f(j)).$$$

Lean4

theorem partialSups_disjoint_of_disjoint (f : ι → α) (h : Pairwise (Disjoint on f)) {i j : ι} (hij : i < j) :
    Disjoint (partialSups f i) (f j) :=
  disjoint_partialSups_left.2 fun _ hk ↦ h (hk.trans_lt hij).ne

Похожие утверждения