term𝓘(_) — Mathlib

English

The function-valued coercion is defined by the underlying toFun', which is itself defined as the toFun of the partial equivalence underlying the model.

Русский

Приведение к функциям задается через toFun', который определяется как toFun частичного эквалентного отображения модели.

LaTeX

$$$toFun' : ModelWithCorners 𝕜 E H \\to (H \\to E)$$$

Lean4

/-- A normed field is a model with corners. -/
@[scoped term_parser 1000]
public meta def «term𝓘(_)» : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `Manifold.«term𝓘(_)» 1024
    (ParserDescr.binary✝ `andthen (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "𝓘(") (ParserDescr.cat✝ `term 0))
      (ParserDescr.symbol✝ ")"))

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