_aux_Mathlib_Topology_Homotopy_HomotopyGroup___macroRules_Topology_Homotopy_termΩ^_1

English

There is a continuous evaluation map on GenLoop, sending a loop to its value at a fixed point y ∈ N → I.

Русский

Существует непрерывное отображение оценки на GenLoop, отправляющее петлю в её значение в фиксированной точке y.

LaTeX

$$instContinuousEval : ContinuousEval (Ω^N X x) (I^N) X$$

Lean4

@[scoped macro Topology.Homotopy.«termΩ^»]
public meta def «_aux_Mathlib_Topology_Homotopy_HomotopyGroup___macroRules_Topology_Homotopy_termΩ^_1» : Macro✝ := fun
  | `(Ω^) => ``(GenLoop)
  | _ => no_error_if_unused% throw✝ Lean.Macro.Exception.unsupportedSyntax✝

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