Commit 2026-05-04 23:16 d214764e

View on Github →

chore(Order/CompleteLattice/Finset): use to_dual and some golfs (#38851)

Estimated changes

deleted theorem Finset.iInf_biUnion
deleted theorem Finset.iInf_coe
deleted theorem Finset.iInf_finset_image
deleted theorem Finset.iInf_insert
deleted theorem Finset.iInf_insert_update
deleted theorem Finset.iInf_singleton
deleted theorem Finset.iInf_union
deleted theorem iInf_eq_iInf_finset'
deleted theorem iInf_eq_iInf_finset