inf_mul_right

Mathlib.Algebra.Group.Pointwise.Finset.Basic

URI: https://scilib.ai/kg/mathlib#Finset.inf_mul_right

← MathLib Explorer

English

Symmetrically, inf(s * t) f = inf t (λ y, inf s (f (· * y))).

Русский

Симметрично, inf(s * t) f = inf t (λ y, inf s (f (· * y))).

LaTeX

$$inf (s * t) f = inf t (\\lambda y. inf s (f (\\langle ·, y \\rangle)))$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru