compl_sup — Mathlib

English

Complement distributes over supremum: the complement of the supremum of f is the infimum of the complements of f(i).

Русский

Дополнение распределяется над верхней операцией: комплемент объединения равен пересечению комплементов.

LaTeX

$$$\bigg( \bigvee_{i\in s} f(i) \bigg)^{\mathrm{c}} = \bigwedge_{i\in s} (f(i))^{\mathrm{c}}$$$

Lean4

@[simp]
protected theorem compl_sup (s : Finset ι) (f : ι → α) : (s.sup f)ᶜ = s.inf fun i => (f i)ᶜ :=
  map_finset_sup (OrderIso.compl α) _ _

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