Theorem iSupIndep_comp_coe_iff_supIndep

Modification history

2026-02-23 17:11
Mathlib/Order/SupIndep.lean
feat(Order/CompactlyGenerated): remove injectivity hypothesis in `iSupIndep_iff_supIndep_of_injOn` (#35475) …
Added iSupIndep_comp_coe_iff_supIndepView on Github →