isLeast_image2_of_isGreatest — Mathlib

English

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

Русский

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

LaTeX

$$IsLeast s a \rightarrow IsGreatest t b \rightarrow IsLeast (image2 f s t) (f a b)$$

Lean4

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

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