Commit 2022-08-03 16:27 c5e83e00

View on Github →

chore(analysis/convex/cone): set_like instance (#15715) This removes lots of lemmas that are already in the set_like namespace. convex_cone.ext' is now set_like.coe_injective.

Estimated changes

Modified src/analysis/convex/cone.lean

modified theorem convex_cone.comap_id

deleted theorem convex_cone.ext'

modified theorem convex_cone.ext

modified theorem convex_cone.map_id

deleted theorem convex_cone.mem_coe