Theorem generateFrom_insert_empty

Modification history

2024-09-17 11:41
Mathlib/Topology/Order.lean
feat(Topology/Order): Sierpiński space classifies open sets of Scott topology (#16826) …
Added generateFrom_insert_emptyView on Github →