pairwiseDisjoint_insert_of_notMem

English

If i ∉ s, then (insert i s).PairwiseDisjoint f holds iff s.PairwiseDisjoint f and ∀ j∈s, Disjoint (f i) (f j).

Русский

Если i ∉ s, то (insert i s).PairwiseDisjoint f эквивалентно s.PairwiseDisjoint f и ∀ j∈s, Disjoint (f i) (f j).

LaTeX

$${i} (hi : i ∉ s) : (insert i s).PairwiseDisjoint f ↔ s.PairwiseDisjoint f ∧ ∀ j ∈ s, Disjoint (f i) (f j)$$

Lean4

theorem pairwiseDisjoint_insert_of_notMem {i : ι} (hi : i ∉ s) :
    (insert i s).PairwiseDisjoint f ↔ s.PairwiseDisjoint f ∧ ∀ j ∈ s, Disjoint (f i) (f j) :=
  pairwise_insert_of_symmetric_of_notMem (symmetric_disjoint.comap f) hi

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