setoid — Mathlib

English

The setoid on Path x0 x1 is defined by Homotopic.

Русский

Множество-эквивалентность на Path x0 x1 задаётся через отношение Homotopic.

LaTeX

$$$\text{Path.Homotopic.setoid}(x_0,x_1) = \langle Path\, x_0 x_1, \sim_{Homotopic} \rangle$$$

Lean4

/-- The setoid on `Path`s defined by the equivalence relation `Path.Homotopic`. That is, two paths are
equivalent if there is a `Homotopy` between them.
-/
protected def setoid (x₀ x₁ : X) : Setoid (Path x₀ x₁) :=
  ⟨Homotopic, equivalence⟩

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