pairwiseDisjoint_disjointOfUnion — Mathlib

English

There exists K : Set α → Finset (Set α) satisfying disjointness and containment properties for J and C.

Русский

Существуют свойства K, обеспечивающие распад J на непересекающиеся элементы и вложения.

LaTeX

$$$$ \\exists K : Set α \\to Finset (Set α), \\; PairwiseDisjoint J K \\; \\land \\; \\forall i ∈ J, \\; ↑(K i) \\subseteq C $$$$

Lean4

theorem pairwiseDisjoint_disjointOfUnion (hC : IsSetSemiring C) (hJ : ↑J ⊆ C) :
    PairwiseDisjoint J (hC.disjointOfUnion hJ) :=
  (Exists.choose_spec (hC.disjointOfUnion_props hJ)).1

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