Theorem existsUnique_eq_principal_sup_free

Modification history

2026-04-08 12:57
Mathlib/Order/Filter/Cofinite.lean
feat: express filter as supremum of principal filter and free filter (#31242) …
Added existsUnique_eq_principal_sup_freeView on Github →