Commit 2025-03-03 09:04 4c2da682

View on Github →

chore: stop conflating WithTop and Option in WithTop.locallyFiniteOrder (#22477)

Estimated changes

Modified Mathlib/Logic/Embedding/Set.lean

deleted def Function.Embedding.coeWithTop

Modified Mathlib/Order/Hom/Basic.lean

added def Function.Embedding.coeWithTop

Modified Mathlib/Order/Interval/Finset/Defs.lean

added def WithTop.insertTop

added theorem WithTop.some_mem_insertTop

added theorem WithTop.top_mem_insertTop