sup_image₂_le — Mathlib

English

Let g : γ → δ; then sup' (image₂ f s t) h g equals sup' s h.of_image₂_left (fun x => sup' t h.of_image₂_right (g (f x ·))).

Русский

Пусть g : γ → δ; тогда sup' image₂ f s t = sup' s ...

LaTeX

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

Lean4

@[simp (default + 1)] -- otherwise `simp` doesn't use `forall_mem_image₂`

theorem sup_image₂_le {g : γ → δ} {a : δ} : sup (image₂ f s t) g ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, g (f x y) ≤ a := by
  rw [Finset.sup_le_iff, forall_mem_image₂]

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