Mathlib Changelog
v4
Changelog
About
Github
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