term_→Co_ — Mathlib

English

There exists a canonical coercion from F to the type of continuous order-homomorphisms, making F a CoeTC to ContinuousOrderHom.

Русский

Существует каноническое приведение из F в тип непрерывных монотонных отображений, образующее связь CoeTC.

LaTeX

$$instance : CoeTC F (ContinuousOrderHom α β)$$

Lean4

@[inherit_doc ContinuousOrderHom, term_parser 1000]
public meta def «term_→Co_» : Lean.TrailingParserDescr✝ :=
  ParserDescr.trailingNode✝ `«term_→Co_» 25 26
    (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " →Co ") (ParserDescr.cat✝ `term 25))

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