coe_finset_inf — Mathlib

English

For a Finset I and f: I → Closeds α, the underlying set of the finite infimum equals the finite intersection of the underlying sets.

Русский

Для конечного множества и функции, соответствующая пересечение множеств совпадает с пересечением замкнутых множеств.

LaTeX

$$$(sInf f)^{\uparrow} = sInf (\uparrow \circ f).$$$

Lean4

@[simp, norm_cast]
theorem coe_finset_inf (f : ι → Closeds α) (s : Finset ι) : (↑(s.inf f) : Set α) = s.inf ((↑) ∘ f) :=
  map_finset_inf (⟨⟨(↑), coe_inf⟩, coe_top⟩ : InfTopHom (Closeds α) (Set α)) _ _

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