biInf_prod' — Mathlib

English

Let f: β → γ → α, with s ⊆ β and t ⊆ γ. The infimum over the product s × t of the function f, evaluated at x.1 and x.2, equals the iterated infimum over a ∈ s and b ∈ t of f(a, b).

Русский

Пусть f: β → γ → α, s ⊆ β, t ⊆ γ. Тогда инфимум над произведением s × t от функции f, где аргументы идут по нескольким координатам, равен поэторномуinf по a ∈ s и b ∈ t от f(a, b).

LaTeX

$$$\\inf_{x \\in s \\times t} f(x.1, x.2) = \\inf_{a \\in s} \\inf_{b \\in t} f(a, b)$$$

Lean4

theorem biInf_prod' {f : β → γ → α} {s : Set β} {t : Set γ} : ⨅ x ∈ s ×ˢ t, f x.1 x.2 = ⨅ (a ∈ s) (b ∈ t), f a b :=
  biInf_prod

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