compl_iInf — Mathlib

English

Complement commutes with iInf: the complement of the infimum equals the infimum of complements.

Русский

Комплемент сохраняет операцию взятия нижней границы: комплемент ⊓ = ⊓ комплементов.

LaTeX

$$$(\bigwedge_i f(i)).\mathrm{compl} = \bigwedge_i (f(i)).\mathrm{compl}$$$

Lean4

@[simp]
protected theorem compl_iInf (f : ι → UpperSet α) : (⨅ i, f i).compl = ⨅ i, (f i).compl :=
  LowerSet.ext <| by simp only [coe_compl, coe_iInf, compl_iUnion, LowerSet.coe_iInf]

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