seminormFromConst_le_seminorm — Mathlib

English

The function seminormFromConst' hf1 hc hpm is bounded above by f, i.e., seminormFromConst' f x ≤ f x for all x.

Русский

Функция seminormFromConst' ограничена сверху f: для всех x выполняется неравенство.

LaTeX

$$$\forall x,\; \operatorname{seminormFromConst'} hf1 hc hpm x \le f x$$$

Lean4

/-- The function `seminormFromConst' hf1 hc hpm` is bounded above by `f`. -/
theorem seminormFromConst_le_seminorm (x : R) : seminormFromConst' hf1 hc hpm x ≤ f x :=
  by
  apply le_of_tendsto (seminormFromConst_isLimit hf1 hc hpm x)
  simp only [eventually_atTop, ge_iff_le]
  use 1
  intro n hn
  rw [seminormFromConst_seq, div_le_iff₀ (by positivity), ← hpm c hn]
  exact map_mul_le_mul ..

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