bddAbove_image2_of_bddBelow — Mathlib

English

If f is monotone in each argument and s,t are such that upper bounds exist, then the image of upper bounds is contained in upper bounds of the image.

Русский

Если f монотонна по каждому аргументу и существуют верхние границы для s и t, то image2 f (upperBounds s) (upperBounds t) ⊆ upperBounds (image2 f s t).

LaTeX

$$$ image2 f (upperBounds s) (upperBounds t) \subseteq upperBounds (image2 f s t) $$$

Lean4

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

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