inf_mul_left — Mathlib

English

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

Русский

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

LaTeX

$$inf (s * t) f = inf s (\\lambda x. inf t (f (x * ·)))$$

Lean4

@[to_additive]
theorem inf_mul_left {β} [SemilatticeInf β] [OrderTop β] (s t : Finset α) (f : α → β) :
    inf (s * t) f = inf s fun x ↦ inf t (f <| x * ·) :=
  inf_image₂_left ..

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