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 α) _ _