sInf_apply — Mathlib

English

Let α be a type, β a family of types β a, and s a set of functions a ↦ β a. Then the infimum over s of the function values at a equals the infimum over f ∈ s of f(a).

Русский

Пусть α — тип, β — семейство типов β(a), и s — множество функций a ↦ β(a). Тогда инфимуум по s значений в точке a равен инфимууму по f ∈ s: sInf s a = inf_{f∈s} f(a).

LaTeX

$$$\\displaystyle s\\!\\inf s\\; a = \\inf_{f \\in s} f(a)$$$

Lean4

@[simp]
theorem sInf_apply {α : Type*} {β : α → Type*} [∀ i, InfSet (β i)] {s : Set (∀ a, β a)} {a : α} :
    sInf s a = ⨅ f : s, (f : ∀ a, β a) a :=
  rfl

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