Theorem generateFrom_insert_univ

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_univView on Github →