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.