seminormFromConst_isLimit — Mathlib

English

The function seminormFromConst' hf1 hc hpm is power-multiplicative: for any x and m, seminormFromConst' (x^m) = (seminormFromConst' x)^m.

Русский

Функция seminormFromConst' является степенной-мультипликативной: для любого x и натурального m выполняется seminormFromConst'(x^m) = (seminormFromConst'(x))^m.

LaTeX

$$IsPowMul (seminormFromConst' hf1 hc hpm)$$

Lean4

/-- We prove that `seminormFromConst' hf1 hc hpm x` is the limit of the sequence
  `seminormFromConst_seq c f x` as `n` tends to infinity. -/
theorem seminormFromConst_isLimit (x : R) :
    Tendsto (seminormFromConst_seq c f x) atTop (𝓝 (seminormFromConst' hf1 hc hpm x)) :=
  (Real.tendsto_of_bddBelow_antitone (seminormFromConst_bddBelow c f x)
      (seminormFromConst_seq_antitone hf1 hc hpm x)).choose_spec

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