compl_iInf — Mathlib

English

For any family of lower sets f i, the complement distributes over the infimum: (⨅ i, f i).compl = ⨅ i, (f i).compl.

Русский

Для произвольной семейной функции нижних множеств справедливo: (⨅ i, f i).compl = ⨅ i, (f i).compl.

LaTeX

$$$ (\big \wedge_i f_i).\mathrm{compl} = \big \wedge_i (f_i).\mathrm{compl} $$$

Lean4

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

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