pairwiseDisjoint — Mathlib

English

The open cells cover the universe in a pairwise disjoint manner.

Русский

Открытые клетки образуют попарно непересекающееся покрытие всей области.

LaTeX

$$$(univ : Set (\\Sigma n, cell C n)).PairwiseDisjoint (\\lambda ni, openCell ni.1 ni.2)$$$

Lean4

theorem pairwiseDisjoint [RelCWComplex C D] :
    (univ : Set (Σ n, cell C n)).PairwiseDisjoint (fun ni ↦ openCell ni.1 ni.2) :=
  RelCWComplex.pairwiseDisjoint'

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