Commit 2025-01-13 17:41 14815c9c
View on Github →feat: lemmas about the left and right boundary point under Icc{Left,Right}Chart (#15891)
Another step towards proving that a non-empty the real interval $[x,y]$ has boundary ${ x,y }$ (as a manifold).
Add missing Icc.coe_top and Icc.coe_bot lemmas.