toLp_fst

Mathlib.Analysis.Normed.Lp.ProdLp

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

English

The first coordinate is preserved under the toLp map: (toLp p (x, y)).fst = x.

Русский

Первая координата сохраняется через отображение toLp: (toLp p (x,y)).fst = x.

LaTeX

$$$\mathrm{toLp}_p(x,y).\mathrm{fst} = x$$$

Lean4

@[simp]
theorem toLp_fst (x : α × β) : (toLp p x).fst = x.fst :=
  rfl

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

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

Разделы

Аффилиация

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