disjointOfDiffUnion_subset — Mathlib

English

The underlying set of the disjointOfDiffUnion is a subset of C.

Русский

Обезличенная совокупность disjointOfDiffUnion является подмножеством C.

LaTeX

$$$$ ↑(hC.disjointOfDiffUnion hs hI) \\\\subseteq C $$$$

Lean4

theorem disjointOfDiffUnion_subset (hC : IsSetSemiring C) (hs : s ∈ C) (hI : ↑I ⊆ C) :
    ↑(hC.disjointOfDiffUnion hs hI) ⊆ C := by
  classical
  simp only [disjointOfDiffUnion, coe_sdiff, coe_singleton, diff_singleton_subset_iff]
  exact (hC.exists_disjoint_finset_diff_eq hs hI).choose_spec.1.trans (Set.subset_insert _ _)

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