inf_product_right — Mathlib

English

Same as Inf ProdMap dual under order dual; inf over product equals inf over dual product.

Русский

То же самое, что и Inf ProdMap через порядок-перевод; inf по произведению равно inf по двойному произведению.

LaTeX

$$inf (s ×ˢ t) (Prod.map f g) = (inf s f, inf t g)$$

Lean4

theorem inf_product_right (s : Finset β) (t : Finset γ) (f : β × γ → α) :
    (s ×ˢ t).inf f = t.inf fun i' => s.inf fun i => f ⟨i, i'⟩ :=
  @sup_product_right αᵒᵈ _ _ _ _ _ _ _

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