schwartzSeminormFamily_apply_zero

English

The evaluation of the seminorm family at a particular pair (n,k) matches the original seminorm on SchwartzMap.

Русский

Значение семинормы семейства в конкретной паре (n,k) совпадает с исходной семинормой на SchwartzMap.

LaTeX

$$$\mathrm{schwartzSeminormFamily}(\mathbb{K},E,F)(n,k)=\mathrm{SchwartzMap.seminorm}\ \mathbb{K}\ n\ k$$$

Lean4

@[simp]
theorem schwartzSeminormFamily_apply_zero : schwartzSeminormFamily 𝕜 E F 0 = SchwartzMap.seminorm 𝕜 0 0 :=
  rfl

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