coe_finsetInf' — Mathlib

English

For a nonempty finite index set s and a family f_i ∈ C_c(α, β), the pointwise infimum commutes with taking function values; the map s.inf' H f, when viewed as a function α → β, coincides with the infimum over i of the functions f_i.

Русский

Для ненулевого конечного множества индексов s и семейства f_i ∈ C_c(α, β) точечный инфимум согласуется с приведением к функциям: функция (s.inf' H f) viewed as α → β совпадает с infimum по i функций f_i.

LaTeX

$$$$\forall a \in \alpha,\ (s\inf' H f)(a) = \inf_{i \in s} f_i(a).$$$$

Lean4

@[simp, norm_cast]
theorem coe_finsetInf' {ι : Type*} {s : Finset ι} (H : s.Nonempty) (f : ι → C_c(α, β)) :
    ⇑(s.inf' H f) = s.inf' H fun i ↦ ⇑(f i) := by ext; simp [finsetInf'_apply]

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