pairwiseDisjoint_union — Mathlib

English

If s and t are PairwiseDisjoint under f and every element of s is disjoint from every element of t, then s ∪ t is PairwiseDisjoint under f.

Русский

Если s и t попарно непересекаются относительно f и элементы из s непересекаются с элементами из t, то s ∪ t попарно непересекается относительно f.

LaTeX

$$s.PairwiseDisjoint f → t.PairwiseDisjoint f → (∀ i ∈ s, ∀ j ∈ t, i ≠ j → Disjoint (f i) (f j)) → (s ∪ t).PairwiseDisjoint f$$

Lean4

theorem pairwiseDisjoint_union :
    (s ∪ t).PairwiseDisjoint f ↔
      s.PairwiseDisjoint f ∧ t.PairwiseDisjoint f ∧ ∀ ⦃i⦄, i ∈ s → ∀ ⦃j⦄, j ∈ t → i ≠ j → Disjoint (f i) (f j) :=
  pairwise_union_of_symmetric <| symmetric_disjoint.comap f

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