inf_apply — Mathlib

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

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