Theorem generateFrom_insert_of_generateOpen

Modification history

2024-07-15 16:11
Mathlib/Topology/Order.lean
feat(Mathlib/Topology/Bases): subbasis closed under intersection is a basis (#12221) …
Added generateFrom_insert_of_generateOpenView on Github →