Def TopCat.isInitialPempty

Modification history

2023-05-09 06:29

Mathlib/Topology/Category/Top/Limits/Basic.lean

chore: tidy various files (#3848)

Deleted TopCat.isInitialPempty View on Github →

2023-05-05 22:16

Mathlib/Topology/Category/Top/Limits/Basic.lean

chore: forward-port backports (#3752) …

Added TopCat.isInitialPempty View on Github →