inf'_image₂_right — Mathlib

English

Let s ⊆ α and t ⊆ β be finite, and g: γ → δ. The infimum of g over image₂ f s t equals the iterated infimum with t outer: inf over y in t of inf over x in s of g(f(x,y)).

Русский

Пусть s ⊆ α и t ⊆ β — конечные, и g: γ → δ. Нижний предел функции g на image₂ f s t равен inf_{y∈t} inf_{x∈s} g(f(x,y)).

LaTeX

$$$\displaystyle \inf\big(\operatorname{image}_2 f s t\big) g = \inf\!\; t\; (\inf'\; s\; (g\circ f))$$$

Lean4

theorem inf'_image₂_right (g : γ → δ) (h : (image₂ f s t).Nonempty) :
    inf' (image₂ f s t) h g = inf' t h.of_image₂_right fun y ↦ inf' s h.of_image₂_left (g <| f · y) :=
  sup'_image₂_right (δ := δᵒᵈ) g h

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