sup_mul_left — Mathlib

English

The supremum of the product equals the supremum over the left factor of the sup over the right factor: sup(s * t) f = sup s (λ x, sup t (f (x * ·))).

Русский

Наибольшая верхняя грань произведения равна верхней грани по левой части в виде отражения: sup(s * t) f = sup s (λ x, sup t (f (x * ·))).

LaTeX

$$sup (s * t) f = sup s (\\lambda x. sup t (f \\langle x, · \\rangle))$$

Lean4

@[to_additive]
theorem sup_mul_left {β} [SemilatticeSup β] [OrderBot β] (s t : Finset α) (f : α → β) :
    sup (s * t) f = sup s fun x ↦ sup t (f <| x * ·) :=
  sup_image₂_left ..

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