sUnion_disjointOfDiffUnion_subset

Mathlib.MeasureTheory.SetSemiring

URI: https://scilib.ai/kg/mathlib#MeasureTheory.IsSetSemiring.sUnion_disjointOfDiffUnion_subset

← MathLib Explorer

English

If t is a member of hC.disjointOfDiffUnion hs hI, then t ⊆ s.

Русский

Если t является элементом hC.disjointOfDiffUnion hs hI, то t ⊆ s.

LaTeX

$$$$ t \\\\subseteq s $$$$

Lean4

theorem sUnion_disjointOfDiffUnion_subset (hC : IsSetSemiring C) (hs : s ∈ C) (hI : ↑I ⊆ C) :
    ⋃₀ (hC.disjointOfDiffUnion hs hI : Set (Set α)) ⊆ s :=
  by
  rw [← hC.diff_sUnion_eq_sUnion_disjointOfDiffUnion]
  exact diff_subset

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru