image2 — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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