insert — Mathlib

English

Inserting i into s under a suitable condition yields (insert i s).PairwiseDisjoint f.

Русский

При определенном условии добавление i в s дает (insert i s).PairwiseDisjoint f.

LaTeX

$$Set.PairwiseDisjoint.insert (hs : s.PairwiseDisjoint f) {i : ι} (h : ∀ j ∈ s, i ≠ j → Disjoint (f i) (f j)) : (insert i s).PairwiseDisjoint f$$

Lean4

protected theorem insert (hs : s.PairwiseDisjoint f) {i : ι} (h : ∀ j ∈ s, i ≠ j → Disjoint (f i) (f j)) :
    (insert i s).PairwiseDisjoint f :=
  pairwiseDisjoint_insert.2 ⟨hs, h⟩

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