inf_prodMap — Mathlib

English

Dual of Inf Product Left: inf over s ×ˢ t of f equals inf over i' of (s inf f) with i' varying in t.

Русский

Двоично-правое: inf по s ×ˢ t от f равен inf по i' из t от (s inf f).

LaTeX

$$inf (s ×ˢ t) (f) = t.inf (\\lambda i'. s.inf (\\lambda i. f(i,i'))) $$

Lean4

@[simp]
theorem inf_prodMap (hs : s.Nonempty) (ht : t.Nonempty) (f : ι → α) (g : κ → β) :
    inf (s ×ˢ t) (Prod.map f g) = (inf s f, inf t g) :=
  sup_prodMap (α := αᵒᵈ) (β := βᵒᵈ) hs ht _ _

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