image2_bddAbove — Mathlib

English

If s and t have lower bounds, then image2 f s t has an upper bound; concretely, there exists a ∈ lowerBounds s and b ∈ lowerBounds t such that f a b is an upper bound of image2 f s t.

Русский

Если s и t имеют нижние границы, то image2 f s t имеет верхнюю границу: существует a ∈ lowerBounds s и b ∈ lowerBounds t такие, что f(a,b) является верхней границей image2 f s t.

LaTeX

$$BddBelow s → BddBelow t → BddAbove (Set.image2 f s t)$$

Lean4

theorem image2_bddAbove : BddBelow s → BddBelow t → BddAbove (Set.image2 f s t) :=
  by
  rintro ⟨a, ha⟩ ⟨b, hb⟩
  exact ⟨f a b, mem_upperBounds_image2_of_mem_lowerBounds h₀ h₁ ha hb⟩

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