Homotopic — Mathlib

English

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

Русский

Осуществляется фактор-множество Path x0 x1 по эквивалентности Homotopic.

LaTeX

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

Lean4

/-- Two paths `p₀` and `p₁` are `Path.Homotopic` if there exists a `Homotopy` between them.
-/
def Homotopic (p₀ p₁ : Path x₀ x₁) : Prop :=
  Nonempty (p₀.Homotopy p₁)

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