termC₀(_,_) — Mathlib

English

There is a can-lift structure showing how to lift a partial continuous map into a full map into units given compatibility with evaluation maps.

Русский

Существует конструкция canLift, показывающая как частичное непрерывное отображение можно поднять до полного отображения в единицы при совместимости с оценочными отображениями.

LaTeX

$$$\text{CanLift } C(X,R)\; C(X,R^{\times})$ with appropriate lifting data.$$

Lean4

@[inherit_doc ZeroAtInftyContinuousMap, scoped term_parser 2000]
public meta def «termC₀(_,_)» : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `ZeroAtInfty.«termC₀(_,_)» 1024
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen
          (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "C₀(") (ParserDescr.cat✝ `term 0))
          (ParserDescr.symbol✝ ", "))
        (ParserDescr.cat✝ `term 0))
      (ParserDescr.symbol✝ ")"))

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