proj_equiv₁'

Mathlib.Data.Fin.Tuple.Sort

URI: https://scilib.ai/kg/mathlib#Tuple.proj_equiv₁'

English

Proj ∘ graphEquiv1 f = f.

Русский

Proj ∘ graphEquiv1 f = f.

LaTeX

$$$\\mathrm{graph.proj} \\circ \\mathrm{graphEquiv}_1(f) = f$$$

Lean4

@[simp]
theorem proj_equiv₁' (f : Fin n → α) : graph.proj ∘ graphEquiv₁ f = f :=
  rfl

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

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

Разделы

Аффилиация

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