inf'_apply — Mathlib

English

Same as Sup' Apply: (s.sup' H f) (b) = sup_{a∈s} f(a)(b).

Русский

То же самое, что и выше: (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 inf'_apply {C : β → Type*} [∀ b : β, SemilatticeInf (C b)] {s : Finset α} (H : s.Nonempty)
    (f : α → ∀ b : β, C b) (b : β) : s.inf' H f b = s.inf' H fun a => f a b :=
  Finset.sup'_apply (C := fun b => (C b)ᵒᵈ) H f b

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