image2_bddBelow — Mathlib

English

If s and t have upper bounds and f is monotone in the second argument and antitone in the first argument, then image2 f s t is bounded below; i.e., there exists a lower bound for image2 f s t.

Русский

Если s и t ограничены сверху, а f(·,·) монотонна по второму аргументу и антимонотонна по первому, то image2 f s t ограничено снизу.

LaTeX

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

Lean4

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

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