isGreatest_image2_of_isLeast — Mathlib

English

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

Русский

Если a максимален в s и b минимален в t, то f(a,b) максимален в image2 f s t.

LaTeX

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

Lean4

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

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