Commit 2024-12-31 11:21 8d758ea2

View on Github →

feat(Topology): add Dense.induction (#20342) This can be used as

induction x using hs.induction with
| mem x hx => sorry
| isClosed => sorry

when hs : Dense s

Estimated changes

added theorem Dense.induction