iInf_image2 — Mathlib

English

Let f: β → γ → α, s ⊆ β, t ⊆ γ, and g: δ → α. Then the infimum over image2 f s t of g equals the iterated infimum over b ∈ s and c ∈ t of g(f b c).

Русский

Пусть f: β → γ → α, s ⊆ β, t ⊆ γ, и g: δ → α. Тогда инфимуум над образованием image2 f над s×t удовлетворяет: inf_{d ∈ image2 f s t} g(d) = inf_{b ∈ s} inf_{c ∈ t} g(f(b,c)).

LaTeX

$$$\\inf_{d \\in \\mathrm{image2}\\,f\\,s\\,t} g(d) = \\inf_{b \\in s} \\inf_{c \\in t} g(f(b,c))$$$

Lean4

theorem iInf_image2 {γ δ} (f : β → γ → δ) (s : Set β) (t : Set γ) (g : δ → α) :
    ⨅ d ∈ image2 f s t, g d = ⨅ b ∈ s, ⨅ c ∈ t, g (f b c) :=
  iSup_image2 f s t (toDual ∘ g)

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