leanprover-community.github.io
leanprover-community.github.io copied to clipboard
yaml parsing has bug with same-title entries
In the section "Hilbert spaces" of the undergrad.yaml
file, there are two entries called "its completeness". It makes sense in context:
...
dual space: 'normed_space.dual.normed_space'
Riesz representation theorem: 'inner_product_space.to_dual'
inner product space $l^2$: 'lp.inner_product_space'
its completeness: 'lp.complete_space'
inner product space $L^2$: 'measure_theory.L2.inner_product_space'
its completeness: 'measure_theory.Lp.complete_space'
...
On the current display of the website, the first "its completeness" links to entry for the second "its completeness", and the second "its completeness" does not appear at all.
I don't think it's worth making that code much more complicated for one example where we could simply change to "completeness of $l^2$" and "completeness of $L^2$"