union — Mathlib

English

Given hs and ht and cross-disjointness, the union has PairwiseDisjoint f.

Русский

При наличии попарной непересекаемости для s и t и условии попарной непересекаемости между ними, объединение является попарно непересекаемым.

LaTeX

$$Set.PairwiseDisjoint.union (hs : s.PairwiseDisjoint f) (ht : t.PairwiseDisjoint f) (h : ∀ ⦃i⦄, i ∈ s → ∀ ⦃j⦄, j ∈ t → i ≠ j → Disjoint (f i) (f j)) : (s ∪ t).PairwiseDisjoint f$$

Lean4

theorem union (hs : s.PairwiseDisjoint f) (ht : t.PairwiseDisjoint f)
    (h : ∀ ⦃i⦄, i ∈ s → ∀ ⦃j⦄, j ∈ t → i ≠ j → Disjoint (f i) (f j)) : (s ∪ t).PairwiseDisjoint f :=
  pairwiseDisjoint_union.2
    ⟨hs, ht, h⟩
      -- classical

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