insert_of_notMem — Mathlib

English

If hs is PairwiseDisjoint f and i ∉ s, and h provides disjointness with all in s, then (insert i s).PairwiseDisjoint f.

Русский

Если hs — попарная непересечение по f и i ∉ s и для всех j∈s выполнено Disjoint(f i, f j), то (insert i s).PairwiseDisjoint f.

LaTeX

$$(pairwiseDisjoint_insert_of_notMem hi).2 ⟨hs, h⟩$$

Lean4

theorem insert_of_notMem (hs : s.PairwiseDisjoint f) {i : ι} (hi : i ∉ s) (h : ∀ j ∈ s, Disjoint (f i) (f j)) :
    (insert i s).PairwiseDisjoint f :=
  (pairwiseDisjoint_insert_of_notMem hi).2 ⟨hs, h⟩

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