Theorem OrderIso.map_sInf_eq_sInf_symm_preimage

Modification history

2026-03-20 14:17
Mathlib/Order/CompleteLattice/Basic.lean
chore: use @[to_dual] extensively in CompleteLattice (#35209) …
Deleted OrderIso.map_sInf_eq_sInf_symm_preimageView on Github →
2024-01-26 19:09
Mathlib/Order/CompleteLattice.lean
feat: Add lattice lemmas about `Sub{group,monoid}.{op,unop}` (#9860) …
Added OrderIso.map_sInf_eq_sInf_symm_preimageView on Github →