term_→ᴬ[_]_ — Mathlib

English

Affine spaces are associative under product, up to a continuous affine equivalence: (P₁ × P₂) × P₃ ≃ᴬ[k] P₁ × (P₂ × P₃).

Русский

Аффинные пространства ассоциативны по произведению, до непрерывной аффинной эквивалентности: (P₁ × P₂) × P₃ ≃ᴬ[k] P₁ × (P₂ × P₃).

LaTeX

$$$\text{prodAssoc} : (P_1 \times P_2) \times P_3 \simeq_{Aff}^k P_1 \times (P_2 \times P_3).$$$

Lean4

/-- A continuous map of affine spaces -/
@[term_parser 1000]
public meta def «term_→ᴬ[_]_» : Lean.TrailingParserDescr✝ :=
  ParserDescr.trailingNode✝ `«term_→ᴬ[_]_» 25 0
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " →ᴬ[") (ParserDescr.cat✝ `term 0))
        (ParserDescr.symbol✝ "] "))
      (ParserDescr.cat✝ `term 0))

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