compl_inf — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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