seminormFromConst_seq_def

Mathlib.Analysis.Normed.Unbundled.SeminormFromConst

URI: https://scilib.ai/kg/mathlib#seminormFromConst_seq_def

English

The value seminormFromConst_seq c f x is defined by the formula n ↦ f(x c^n)/f(c^n).

Русский

Значение seminormFromConst_seq c f x определяется как $n \mapsto f(x c^n)/f(c^n)$.

LaTeX

$$$seminormFromConstSeq(c,f,x) = (\lambda n. \dfrac{f(x c^n)}{f(c^n)})$$$

Lean4

theorem seminormFromConst_seq_def (x : R) : seminormFromConst_seq c f x = fun n ↦ f (x * c ^ n) / f c ^ n :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru