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.

Estimated changes