English
Let α be a topological space and β a semilattice with infimum, and let f_i ∈ C_c(α, β) for i in a nonempty finite set s. Then the pointwise infimum of the family (f_i) is given by the map a ↦ inf_{i∈s} f_i(a); equivalently, (s.inf' H f)(a) = inf_{i∈s} f_i(a) for all a ∈ α.
Русский
Пусть α – топологическое множество, β – полулинейное полузаданное множество с инфимумом, и пусть для каждого i в ненулевом конечном множестве s имеется f_i ∈ C_c(α, β). Тогда покоординатный инфимум семейства (f_i) задаётся по точкам: для каждого a ∈ α выполняется (s.inf' H f)(a) = inf_{i∈s} f_i(a).
LaTeX
$$$$\forall a \in \alpha,\ (s\inf' H f)(a) = \inf_{i \in s} f_i(a).$$$$
Lean4
theorem finsetInf'_apply {ι : Type*} {s : Finset ι} (H : s.Nonempty) (f : ι → C_c(α, β)) (a : α) :
s.inf' H f a = s.inf' H fun i ↦ f i a :=
Finset.comp_inf'_eq_inf'_comp H (fun g : C_c(α, β) ↦ g a) fun _ _ ↦ rfl
