partialSups_apply — Mathlib

English

In a Pi-type setting, the i-th component of partialSups f is the partialSups of the function x ↦ f x t at i.

Русский

В отношении типа Π, i-й компонент partialSups f равен partialSups функции x ↦ f x t на i.

LaTeX

$$$\\mathrm{partialSups}\\, f\\, i\\; t = \\mathrm{partialSups}\\, (f \\cdot t)\\, i$$$

Lean4

protected theorem partialSups_apply {τ : Type*} {π : τ → Type*} [∀ t, SemilatticeSup (π t)] (f : ι → (t : τ) → π t)
    (i : ι) (t : τ) : partialSups f i t = partialSups (f · t) i := by simp only [partialSups_apply, Finset.sup'_apply]

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