instZero

Mathlib.Analysis.Normed.Unbundled.RingSeminorm

URI: https://scilib.ai/kg/mathlib#RingSeminorm.instZero

English

If two RingSeminorms agree on all inputs, they are equal.

Русский

Если две RingSeminorm совпадают на всех аргументах, они равны.

LaTeX

$$p = q if ∀ x, p x = q x$$

Lean4

instance : Zero (RingSeminorm R) :=
  ⟨{ AddGroupSeminorm.instZeroAddGroupSeminorm.zero with mul_le' := fun _ _ => (zero_mul _).ge }⟩

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

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

Разделы

Аффилиация

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