Theorem TopologicalSpace.Opens.set_range_inclusion'

Modification history

2024-10-17 08:51

Mathlib/Topology/Category/TopCat/Opens.lean

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

Added TopologicalSpace.Opens.set_range_inclusion'View on Github →