interpStrip_eq_of_zero — Mathlib

English

Let f: C → E as above. If sSupNormIm f 0 = 0 or sSupNormIm f 1 = 0, then interpStrip f z = 0 for all z.

Русский

Пусть f: ℂ → E как выше. Если sSupNormIm f 0 = 0 или sSupNormIm f 1 = 0, то interpStrip f z = 0 для всех z.

LaTeX

$$$\\displaystyle \\text{If } sSupNormIm f 0 = 0 \\text{ or } sSupNormIm f 1 = 0,\\; \\interpStrip f z = 0.$$$

Lean4

/-- Rewrite for `InterpStrip` when `0 = sSupNormIm f 0` or `0 = sSupNormIm f 1`. -/
theorem interpStrip_eq_of_zero (z : ℂ) (h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0) : interpStrip f z = 0 :=
  if_pos h

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