Iic_sInf — Mathlib

English

The principal lower set of the infimum over a set equals the infimum of the principal lower sets: Iic(sInf S) = ⨅ a∈S, Iic a.

Русский

Порожденное нижнее множество от sInf S равно infimum множителей порожденных нижних множеств: Iic(sInf S) = ⨅ a∈S, Iic a.

LaTeX

$$Iic (sInf S) = ⨅ a ∈ S, Iic a$$

Lean4

@[simp]
theorem Iic_sInf (S : Set α) : Iic (sInf S) = ⨅ a ∈ S, Iic a :=
  SetLike.ext fun c => by simp only [mem_Iic_iff, mem_iInf₂_iff, le_sInf_iff]

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