sup'_apply — Mathlib

English

Let s be a nonempty finite subset of α and f: α → ∀ β, C β. Then (s.sup' H f) (b) = sup_{a∈s} f(a)(b).

Русский

Пусть s — непустое конечное подмножество α и f: α → ∀ β, C β. Тогда (s.sup' H f)(b) = sup_{a∈s} f(a)(b).

LaTeX

$$$s \neq \varnothing \Rightarrow (s.sup' H f)(b) = \sup_{a \in s} f(a)(b).$$$

Lean4

@[simp]
protected theorem sup'_apply {C : β → Type*} [∀ b : β, SemilatticeSup (C b)] {s : Finset α} (H : s.Nonempty)
    (f : α → ∀ b : β, C b) (b : β) : s.sup' H f b = s.sup' H fun a => f a b :=
  comp_sup'_eq_sup'_comp H (fun x : ∀ b : β, C b => x b) fun _ _ => rfl

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