pairwiseDisjoint — Mathlib

English

If Pairwise (Disjoint on f) holds, then for any s, s.PairwiseDisjoint f holds.

Русский

Если выполняется попарная совместимость через Disjoint (на f), тогда для любого s выполняется попарная непересекаемость.

LaTeX

$$h : Pairwise (Disjoint on f) ⇒ ∀ s, s.PairwiseDisjoint f$$

Lean4

/-- If the range of `f` is pairwise disjoint, then the image of any set `s` under `f` is as well. -/
theorem _root_.Pairwise.pairwiseDisjoint (h : Pairwise (Disjoint on f)) (s : Set ι) : s.PairwiseDisjoint f :=
  h.set_pairwise s

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