English
Let g : γ → δ. If (image₂ f s t).Nonempty, then a ≤ inf' (image₂ f s t) h g holds iff for all x ∈ s and y ∈ t, a ≤ g (f x y).
Русский
Пусть g : γ → δ. Если (image₂ f s t) непусто, то a ≤ inf' (image₂ f s t) задаётся эквивалентно ∀ x ∈ s, ∀ y ∈ t, a ≤ g (f x y).
LaTeX
$$$\\forall s:\\ Finset, t:\\ Finset, (image_2 f s t).Nonempty \\Rightarrow (a \\leq inf' (image_2 f s t) h g) \\Leftrightarrow (\\forall x\\in s, \\forall y\\in t, a \\le g (f x y))$$$
Lean4
@[simp (default + 1)] -- otherwise `simp` doesn't use `forall_mem_image₂`
theorem le_inf'_image₂ {g : γ → δ} {a : δ} (h : (image₂ f s t).Nonempty) :
a ≤ inf' (image₂ f s t) h g ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ g (f x y) := by rw [le_inf'_iff, forall_mem_image₂]
