equiv_symm_eq_zero_iff

Mathlib.Analysis.Normed.Lp.WithLp

URI: https://scilib.ai/kg/mathlib#WithLp.equiv_symm_eq_zero_iff

← MathLib Explorer

English

The inverse equivalence of x equals zero iff x = 0.

Русский

Обратная эквивалентность x равна нулю тогда и только тогда, когда x = 0.

LaTeX

$$$(WithLp.equiv p V).\text{symm} x = 0 \iff x = 0$$$

Lean4

@[deprecated toLp_eq_zero (since := "2025-06-08")]
theorem equiv_symm_eq_zero_iff [AddCommGroup V] {x : V} : (WithLp.equiv p V).symm x = 0 ↔ x = 0 :=
  Iff.rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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