image2 — Mathlib

English

If a is a greatest element of s and b is a greatest element of t, then f(a, b) is a greatest element of image2 f s t.

Русский

Если a — наибольший элемент множества s, а b — наибольший элемент множества t, тогда f(a, b) — наибольший элемент множества image2 f s t.

LaTeX

$$$\\big( IsGreatest\\, s\\, a \\big) \\to \\big( IsGreatest\\, t\\, b \\big) \\to IsGreatest(\\operatorname{image2} f\\, s\\, t,\\ f a b)$$$

Lean4

protected theorem image2 (ha : IsGreatest s a) (hb : IsGreatest t b) : IsGreatest (image2 f s t) (f a b) :=
  ⟨mem_image2_of_mem ha.1 hb.1, mem_upperBounds_image2 h₀ h₁ ha.2 hb.2⟩

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