term∑'_,_ — Mathlib

English

Under appropriate conditions, HasProd (f ∘ g) a is equivalent to HasProd f a.

Русский

При соблюдении условий HasProd (f ∘ g) a эквивалентно HasProd f a.

LaTeX

$$$ HasProd (f \circ g) a \leftrightarrow HasProd f a $$$

Lean4

@[inherit_doc tsum, term_parser 1000]
public meta def «term∑'_,_» : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `«term∑'_,_» 1022
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "∑'") Batteries.ExtendedBinder.extBinders)
        (ParserDescr.symbol✝ ", "))
      (ParserDescr.cat✝ `term 67))

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