Theorem TopologicalSpace.Opens.set_range_inclusion'

Modification history

2026-05-01 00:39

Mathlib/Topology/Category/TopCat/Opens.lean

chore(Topology/Category): replace `TopCat` by `TopCat.{u}` (#38779) …

Modified TopologicalSpace.Opens.set_range_inclusion'View on Github →

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 →