Commit 2024-06-19 09:36 ebcc078f

View on Github →

chore(Topology): golf, move (#13935) Golf and move Prod.instNeBotNhdsWithinIio etc.

Estimated changes

added theorem nhdsWithin_mono
deleted theorem nhdsWithin_mono
modified theorem nhdsWithin_pi_eq'
modified theorem nhdsWithin_pi_eq
modified theorem nhdsWithin_pi_eq_bot
modified theorem nhdsWithin_pi_neBot
modified theorem nhdsWithin_pi_univ_eq