Commit 2024-10-17 08:51 7b3af7eb

View on Github →

chore: adjust set_range_forget_map_inclusion' to the statement that is really needed (#17278)

Estimated changes

Modified Mathlib/Topology/Category/TopCat/Opens.lean

deleted theorem TopologicalSpace.Opens.set_range_forget_map_inclusion'

added theorem TopologicalSpace.Opens.set_range_inclusion'

Modified scripts/no_lints_prime_decls.txt