equivQuotient_index

Mathlib.Data.Setoid.Partition

URI: https://scilib.ai/kg/mathlib#IndexedPartition.equivQuotient_index

English

The composition hs.equivQuotient ∘ hs.index equals hs.proj.

Русский

Составная функция hs.equivQuotient ∘ hs.index равна hs.proj.

LaTeX

$$$ hs.equivQuotient \circ hs.index = hs.proj $$$

Lean4

theorem equivQuotient_index : hs.equivQuotient ∘ hs.index = hs.proj :=
  funext hs.equivQuotient_index_apply

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

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

Разделы

Аффилиация

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