sup'_image₂_right — Mathlib

English

Dual to the left version: sup' (image₂ f s t) h g = sup' t h.of_image₂_right (fun y => sup' s h.of_image₂_left (g (f · y))).

Русский

Дуальная левая версия: sup' (image₂ f s t) = sup' t ...

LaTeX

$$$\\forall s:\\ Finset, t:\\ Finset, (image_2 f s t).Nonempty \\Rightarrow sup' (image_2 f s t) h g = sup' t h.of_image_2_right (\\lambda y, sup' s h.of_image_2_left (g (f \\cdot y)))$$$

Lean4

theorem sup'_image₂_right (g : γ → δ) (h : (image₂ f s t).Nonempty) :
    sup' (image₂ f s t) h g = sup' t h.of_image₂_right fun y ↦ sup' s h.of_image₂_left (g <| f · y) := by
  simp only [image₂, sup'_image, sup'_product_right]; rfl

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