pairwiseDisjoint_sUnion — Mathlib

English

Similar to 110320: if not PairwiseDisjoint, there exist i ≠ j with x ∈ f i ∩ f j.

Русский

Как и в 110320: если не попарно непересекается, то существуют i ≠ j и x ∈ f i ∩ f j.

LaTeX

$$$$\exists i \exists j (i \neq j \land \exists x, x \in f(i) \cap f(j)).$$$$

Lean4

theorem pairwiseDisjoint_sUnion {s : Set (Set ι)} (h : DirectedOn (· ⊆ ·) s) :
    (⋃₀ s).PairwiseDisjoint f ↔ ∀ ⦃a⦄, a ∈ s → Set.PairwiseDisjoint a f :=
  pairwise_sUnion h

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