coe_sInf — Mathlib

English

The underlying set of the infimum over a set S of closed subsets is the intersection of all the underlying sets.

Русский

Множество, лежащее в минимальном элементе множества замкнутых подмножеств, равно пересечению их множеств.

LaTeX

$$$(sInf S)^{\uparrow} = \bigcap_{i\in S} \uparrow i.$$$

Lean4

@[simp, norm_cast]
theorem coe_sInf {S : Set (Closeds α)} : (↑(sInf S) : Set α) = ⋂ i ∈ S, ↑i :=
  rfl

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