sUnion_union_disjointOfDiffUnion_of_subset

English

Under subset condition, the union over I of disjointOfDiffUnion combined with sUnion equals s.

Русский

При условии подмножества объединение по I и disjointOfDiffUnion вместе с sUnion равно s.

LaTeX

$$$$ \\bigcup_0 I \\cup \\bigcup_0 hC.disjointOfDiffUnion hs hI = s $$$$

Lean4

theorem sUnion_union_disjointOfDiffUnion_of_subset (hC : IsSetSemiring C) (hs : s ∈ C) (hI : ↑I ⊆ C)
    (hI_ss : ∀ t ∈ I, t ⊆ s) [DecidableEq (Set α)] : ⋃₀ ↑(I ∪ hC.disjointOfDiffUnion hs hI) = s :=
  by
  conv_rhs => rw [← sUnion_union_sUnion_disjointOfDiffUnion_of_subset hC hs hI hI_ss]
  simp_rw [coe_union]
  rw [sUnion_union]

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