HD_below_aux1 — Mathlib

English

Define the auxiliary distance HD on functions f: X×Y → ℝ by HD(f) = max( sup_x inf_y f(inl x, inr y), sup_y inf_x f(inl x, inr y) ).

Русский

Определим вспомогательное расстояние HD на функции f: X×Y → ℝ: HD(f) = max( sup_x inf_y f(inl x, inr y), sup_y inf_x f(inl x, inr y) ).

LaTeX

$$$HD(f) := \max\Big(\sup_{x\in X}(\inf_{y\in Y} f(\mathrm{inl} x, \mathrm{inr} y)),\ \sup_{y\in Y}(\inf_{x\in X} f(\mathrm{inl} x, \mathrm{inr} y))\Big).$$$

Lean4

theorem HD_below_aux1 {f : Cb X Y} (C : ℝ) {x : X} : BddBelow (range fun y : Y => 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)) _) _⟩

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