aedisjoint — Mathlib

English

If a family f is pairwise disjoint, then the corresponding index family is pairwise AEDisjoint.

Русский

Если семейство функций попарно непересекается, то соответствующее индексное семейство AEDisjoint.

LaTeX

$$Pairwise aedisjoint$$

Lean4

protected theorem _root_.Set.PairwiseDisjoint.aedisjoint {f : ι → Set α} {s : Set ι} (hf : s.PairwiseDisjoint f) :
    s.Pairwise (AEDisjoint μ on f) :=
  hf.mono' fun _i _j h => h.aedisjoint

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