sInf_image2 — Mathlib

English

Let f: β → γ → α, s ⊆ β, t ⊆ γ. Then the infimum of the image2 f on s × t equals the iterated infimum over a ∈ s and b ∈ t of f a b.

Русский

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

LaTeX

$$$sInf(\\mathrm{image2}\\,f\\,s\\,t) = \\inf_{a \\in s} \\inf_{b \\in t} f(a,b)$$$

Lean4

theorem sInf_image2 {f : β → γ → α} {s : Set β} {t : Set γ} : sInf (image2 f s t) = ⨅ (a ∈ s) (b ∈ t), f a b := by
  rw [← image_prod, sInf_image, biInf_prod]

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