disjointOfUnion_subset

Mathlib.MeasureTheory.SetSemiring

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

← MathLib Explorer

English

The disjointOfUnion hJ is a subset of C.

Русский

Разделение disjointOfUnion попадает в C.

LaTeX

$$$$ (disjointOfUnion hC hJ j) : Set α \\\\subseteq C $$$$

Lean4

theorem disjointOfUnion_subset (hC : IsSetSemiring C) (hJ : ↑J ⊆ C) (hj : j ∈ J) :
    (disjointOfUnion hC hJ j : Set (Set α)) ⊆ C :=
  (Exists.choose_spec (hC.disjointOfUnion_props hJ)).2.1 _ hj

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

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

Разделы

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

Аффилиация

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