disjointed_eq_inter_compl — Mathlib

English

Disjointed f i can also be expressed as f i intersected with the infimum over j<i of complements of f j.

Русский

Disjointed f i можно записать как пересечение f i и инфимума над j<i комплементов f j.

LaTeX

$$$\forall i:\ ι,\; \operatorname{disjointed} f i = f i \cap \bigwedge_{j

Lean4

theorem disjointed_eq_inter_compl [Preorder ι] [LocallyFiniteOrderBot ι] (f : ι → Set α) (i : ι) :
    disjointed f i = f i ∩ ⋂ j < i, (f j)ᶜ :=
  disjointed_eq_inf_compl f i

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