English
The coercion from a model-with-corners to functions is canonical; the instance provides a uniform way to view model elements as functions.
Π ΡΡΡΠΊΠΈΠΉ
ΠΡΠΈΠ²Π΅Π΄Π΅Π½ΠΈΠ΅ ΠΌΠΎΠ΄Π΅Π»ΠΈ Ρ ΡΠ³Π»Π°ΠΌΠΈ ΠΊ ΡΡΠ½ΠΊΡΠΈΡΠΌ ΠΊΠ°Π½ΠΎΠ½ΠΈΡΠ½ΠΎ; ΡΠΊΠ·Π΅ΠΌΠΏΠ»ΡΡ ΠΎΠ±Π΅ΡΠΏΠ΅ΡΠΈΠ²Π°Π΅Ρ Π΅Π΄ΠΈΠ½ΡΠΉ ΡΠΏΠΎΡΠΎΠ± Π²ΠΈΠ΄Π΅ΡΡ ΡΠ»Π΅ΠΌΠ΅Π½ΡΡ ΠΌΠΎΠ΄Π΅Π»ΠΈ ΠΊΠ°ΠΊ ΡΡΠ½ΠΊΡΠΈΠΈ.
LaTeX
$$$\\text{instance } CoeFun (ModelWithCorners π E H) (\\toFun': H \\to E)$$$
Lean4
@[inherit_doc modelWithCornersSelf, scoped term_parser 1000]
public meta def Β«termπ(_,_)Β» : Lean.ParserDescrβ :=
ParserDescr.nodeβ `Manifold.Β«termπ(_,_)Β» 1024
(ParserDescr.binaryβ `andthen
(ParserDescr.binaryβ `andthen
(ParserDescr.binaryβ `andthen
(ParserDescr.binaryβ `andthen (ParserDescr.symbolβ "π(") (ParserDescr.catβ `term 0))
(ParserDescr.symbolβ ", "))
(ParserDescr.catβ `term 0))
(ParserDescr.symbolβ ")"))
