le_inf_image₂ — Mathlib

English

For finite s ⊆ α, t ⊆ β and g: γ → δ, the statement a ≤ inf(image₂ f s t) g is equivalent to a ≤ g(f x y) for all x∈s and y∈t.

Русский

Для конечных s ⊆ α, t ⊆ β и g: γ → δ верно, что a ≤ inf(image₂ f s t) g тогда и только тогда, когда для всех x∈s и y∈t имеет место a ≤ g(f(x,y)).

LaTeX

$$$a \le \inf (\operatorname{image}_2 f s t)\; g \iff \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 : δ} : a ≤ inf (image₂ f s t) g ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ g (f x y) :=
  sup_image₂_le (δ := δᵒᵈ)

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