Theorem TopologicalSpace.OpenNhds.coe_id

Modification history

2025-02-11 15:35
Mathlib/Topology/Category/TopCat/OpenNhds.lean
refactor: don't use lambdas in `CoeFun` instances (#21405) …
Added TopologicalSpace.OpenNhds.coe_idView on Github →