English
Let s be a nonempty finite subset of α and f: α → ∀ β, C β. Then the value of the supremum at coordinate β equals the supremum over a of f(a)(β).
Русский
Пусть s — непустое конечное подмножество α и f: α → ∀ β, C β. Тогда значение верхней грани в координате β равно супремуму по a: (s.sup f)(β) = sup_{a∈s} f(a)(β).
LaTeX
$$$s \neq \varnothing \Rightarrow s.sup f \;\text{is evaluated coordinatewise: } (s.sup f)(b) = \sup_{a \in s} f(a)(b).$$$
Lean4
@[simp]
protected theorem sup_apply {C : β → Type*} [∀ b : β, SemilatticeSup (C b)] [∀ b : β, OrderBot (C b)] (s : Finset α)
(f : α → ∀ b : β, C b) (b : β) : s.sup f b = s.sup fun a => f a b :=
comp_sup_eq_sup_comp (fun x : ∀ b : β, C b => x b) (fun _ _ => rfl) rfl
