disjoint_accumulate — Mathlib

English

If s is a family of pairwise disjoint sets, then for i < j in a preorder, Accumulate s i is disjoint from s j.

Русский

Если семейство s состоит из попарно непересекающихся множеств, то для i < j в пределе упорядочения Accumulate s i и s j непересекаются.

LaTeX

$$$\\text{Disjoint}(\\mathrm{Accumulate}(s,i), s(j))$ при $i

Lean4

theorem disjoint_accumulate [Preorder α] (hs : Pairwise (Disjoint on s)) {i j : α} (hij : i < j) :
    Disjoint (Accumulate s i) (s j) := by
  apply disjoint_left.2 (fun x hx ↦ ?_)
  simp only [Accumulate, mem_iUnion, exists_prop] at hx
  rcases hx with ⟨k, hk, hx⟩
  exact disjoint_left.1 (hs (hk.trans_lt hij).ne) hx

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