termΩ — Mathlib

English

For i ∈ N and p ∈ GenLoop, the i-th loop extracted from p via toLoop agrees with p when viewed as a continuous map on the cube after composing with the insertion map.

Русский

Для i ∈ N и p ∈ GenLoop, i-я петля, получаемая через toLoop, совпадает с p после композиции с отображением вставки.

LaTeX

$$toLoop i p evaluated equals p after composing with Cube.insertAt i$$

Lean4

@[inherit_doc LoopSpace, scoped term_parser 1000]
public meta def termΩ : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `Topology.Homotopy.termΩ 1024 (ParserDescr.symbol✝ "Ω")

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