English
Let s be a nonempty finite subset of α and f: α → ∀ β, C β. Then the value of the infimum at coordinate β equals the infimum over a of f(a)(β).
Русский
Пусть s — непустое конечное подмножество α и f: α → ∀ β, C β. Тогда значение инфимума по координате β равно инфимума по a: (s.inf f)(β) = Inf_{a∈s} f(a)(β).
LaTeX
$$$s \neq \varnothing \Rightarrow (s.inf\, f)(b) = \inf_{a \in s} f(a)(b).$$$
Lean4
@[simp]
protected theorem inf_apply {C : β → Type*} [∀ b : β, SemilatticeInf (C b)] [∀ b : β, OrderTop (C b)] (s : Finset α)
(f : α → ∀ b : β, C b) (b : β) : s.inf f b = s.inf fun a => f a b :=
Finset.sup_apply (C := fun b => (C b)ᵒᵈ) s f b