self_comp_sort

Mathlib.Data.Fin.Tuple.Sort

URI: https://scilib.ai/kg/mathlib#Tuple.self_comp_sort

← MathLib Explorer

English

The composition f ∘ sort f equals graph.proj ∘ graphEquiv₂ f.

Русский

Составление f ∘ sort f равно graph.proj ∘ graphEquiv₂ f.

LaTeX

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

Lean4

theorem self_comp_sort (f : Fin n → α) : f ∘ sort f = graph.proj ∘ graphEquiv₂ f :=
  show graph.proj ∘ (graphEquiv₁ f ∘ (graphEquiv₁ f).symm) ∘ (graphEquiv₂ f).toEquiv = _ by simp

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

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

Разделы

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

Аффилиация

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