disjointed_eq_inf_compl — Mathlib

English

For every i, disjointed f i equals f i intersected with the infimum over j<i of the complements of f j.

Русский

Для каждого и выполняется: disjointed f i = f i ∩ ⋂_{j<i} (f j)^c.

LaTeX

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

Lean4

theorem disjointed_eq_inf_compl [Preorder ι] [LocallyFiniteOrderBot ι] (f : ι → α) (i : ι) :
    disjointed f i = f i ⊓ ⨅ j < i, (f j)ᶜ := by
  simp only [disjointed_apply, Finset.sup_eq_iSup, mem_Iio, sdiff_eq, compl_iSup]

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