isLeast_image2 — Mathlib

English

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

Русский

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

LaTeX

$$IsGreatest s a → IsGreatest t b → IsLeast (Set.image2 f s t) (f a b)$$

Lean4

theorem isLeast_image2 (ha : IsGreatest 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_upperBounds h₀ h₁ ha.2 hb.2⟩

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