HD_below_aux2 — Mathlib

English

For a fixed x, the range { f(inl x, inr y) + C : y ∈ Y } is bounded below.

Русский

Для фиксированного x множество { f(inl x, inr y) + C : y ∈ Y } ограничено снизу.

LaTeX

$$BddBelow (range fun y : Y => f (inl x, inr y) + C).$$

Lean4

theorem HD_below_aux2 {f : Cb X Y} (C : ℝ) {y : Y} : BddBelow (range fun x : X => f (inl x, inr y) + C) :=
  let ⟨cf, hcf⟩ := f.isBounded_range.bddBelow
  ⟨cf + C, forall_mem_range.2 fun _ => add_le_add_right ((fun x => hcf (mem_range_self x)) _) _⟩

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