disjointed_mem

Mathlib.MeasureTheory.SetSemiring

URI: https://scilib.ai/kg/mathlib#MeasureTheory.IsSetRing.disjointed_mem

← MathLib Explorer

English

If every s(j) ∈ C, then disjointed s i ∈ C for all i.

Русский

Если каждый s(j) ∈ C, то disjointed s i ∈ C для всех i.

LaTeX

$$$\forall i,\ disjointed(s,i) \in C.$$$

Lean4

theorem disjointed_mem {ι : Type*} [Preorder ι] [LocallyFiniteOrderBot ι] (hC : IsSetRing C) {s : ι → Set α}
    (hs : ∀ j, s j ∈ C) (i : ι) : disjointed s i ∈ C :=
  disjointedRec (fun _ j ht ↦ hC.diff_mem ht <| hs j) (hs i)

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

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

Разделы

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

Аффилиация

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