edist_eq_card

Mathlib.Analysis.Normed.Lp.PiLp

URI: https://scilib.ai/kg/mathlib#PiLp.edist_eq_card

English

For p=0, edist is the cardinality of coordinates where edist(f_i,g_i) ≠ 0.

Русский

При p=0 edist равен кардинальности множества координат, где edist(f_i,g_i) ≠ 0.

LaTeX

$$$$edist(f,g)=\\lvert\\{i\\;|\\;edist(f_i,g_i)\\neq 0\\}\\rvert^{\\; }$$$$

Lean4

theorem edist_eq_card (f g : PiLp 0 β) : edist f g = {i | edist (f i) (g i) ≠ 0}.toFinite.toFinset.card :=
  if_pos rfl

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

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

Разделы

Аффилиация

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