subset_of_diffUnion_disjointOfDiffUnion

English

If t ∈ hC.disjointOfDiffUnion hs hI, then t ⊆ s \\ ⋃₀ I.

Русский

Если t ∈ hC.disjointOfDiffUnion hs hI, то t ⊆ s \\ ⋃₀ I.

LaTeX

$$$$ t \\\\subseteq s \\\\setminus ⋃_0 I $$$$

Lean4

theorem subset_of_diffUnion_disjointOfDiffUnion (hC : IsSetSemiring C) (hs : s ∈ C) (hI : ↑I ⊆ C) (t : Set α)
    (ht : t ∈ (hC.disjointOfDiffUnion hs hI : Set (Set α))) : t ⊆ s \ ⋃₀ I :=
  by
  revert t ht
  rw [← sUnion_subset_iff, hC.diff_sUnion_eq_sUnion_disjointOfDiffUnion hs hI]

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