Quotient

Mathlib.Topology.Homotopy.Path

URI: https://scilib.ai/kg/mathlib#Path.Homotopic.Quotient

← MathLib Explorer

English

The quotient on Path x0 x1 by the equivalence relation Homotopic.

Русский

Фактор-множество Path x0 x1 по отношению Homotopic.

LaTeX

$$$\text{Path.Homotopic.Quotient}(x_0,x_1) = \mathrm{Quotient}(\mathrm{Homotopic.setoid}(x_0,x_1))$$$

Lean4

/-- The quotient on `Path x₀ x₁` by the equivalence relation `Path.Homotopic`.
-/
protected def Quotient (x₀ x₁ : X) :=
  Quotient (Homotopic.setoid x₀ x₁)

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

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

Разделы

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

Аффилиация

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