Theorem exists_sSupIndep_disjoint_sSup_atoms

Modification history

2025-07-19 18:49
Mathlib/Order/CompactlyGenerated/Basic.lean
feat: decomposition into independent atoms (#21871) …
Added exists_sSupIndep_disjoint_sSup_atomsView on Github →