Commit 2024-09-11 02:46 23123003

chore: make inner product notation ⟪x, y⟫_𝕜 scoped in namespace InnerProductSpace (#16672) There is a conflict between the Lean-3-style notation ⟪x, y⟫_𝕜 for inner product and the (Lean 4) notation x |_ₗ U ⟪e⟫ for TopCat.Presheaf.restrict that leads to a syntax error in line 125 of Topology/Sheaves/Presheaf.lean when these notations are simultaneously in effect:

  x |_ₗ U ⟪e⟫
        -- ^ unexpected token '⟫'; expected ','

This limitation blocks PR #12502. See this Zulip discussion for details. We resolve the notation conflict by making the inner product notation ⟪x, y⟫_𝕜 scoped in namespace InnerProductSpace and then adding open scoped InnerProductSpace wherever the notation is used.