seminormFromConst' — Mathlib

English

Under appropriate hypotheses, the seminormFromBounded is a norm iff its kernel is trivial, equivalently iff ker f = {0}.

Русский

При соответствующих гипотезах seminormFromBounded является нормой тогда и только тогда, когда его ядро тривиально, то есть ker f = {0}.

LaTeX

$$$\big( \text{conditions on } f \big) \Rightarrow ( (\forall x, (\text{seminormFromBounded} f x = 0) \Rightarrow x=0) \ \Leftrightarrow\ f^{-1}({0})={0} )$$$

Lean4

/-- The real-valued function sending `x ∈ R` to the limit of `(f (x * c^n))/((f c)^n)`. -/
def seminormFromConst' (x : R) : ℝ :=
  (Real.tendsto_of_bddBelow_antitone (seminormFromConst_bddBelow c f x)
      (seminormFromConst_seq_antitone hf1 hc hpm x)).choose

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