norm_lt_sSupNormIm_eps — Mathlib

English

F is bounded by 1 on the verticalClosedStrip boundaries.

Русский

F ограничена сверху единицей на границах вертикальной закрытой полосы.

LaTeX

$$Same as 47585 but with the closed strip.$$

Lean4

/-- Alternative version of `norm_le_sSupNormIm` with a strict inequality and a positive `ε`. -/
theorem norm_lt_sSupNormIm_eps (f : ℂ → E) (ε : ℝ) (hε : ε > 0) (z : ℂ) (hD : z ∈ verticalClosedStrip 0 1)
    (hB : BddAbove ((norm ∘ f) '' verticalClosedStrip 0 1)) : ‖f z‖ < ε + sSupNormIm f (z.re) :=
  lt_add_of_pos_of_le hε (norm_le_sSupNormIm f z hD hB)

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