pairwiseDisjoint_insert — Mathlib

English

Inserting i into s preserves PairwiseDisjoint under f provided f i is disjoint from all f j with j in s, and s is already PD.

Русский

Добавление i в s сохраняет попарность относительно f при условии, что f i непересекается со всеми f j для j в s, и s уже попарно непересекается.

LaTeX

$$(insert i s).PairwiseDisjoint f ↔ (s.PairwiseDisjoint f ∧ ∀ j ∈ s, Disjoint (f i) (f j))$$

Lean4

theorem pairwiseDisjoint_insert {i : ι} :
    (insert i s).PairwiseDisjoint f ↔ s.PairwiseDisjoint f ∧ ∀ j ∈ s, i ≠ j → Disjoint (f i) (f j) :=
  pairwise_insert_of_symmetric <| symmetric_disjoint.comap f

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