Theorem Set.BijOn.iInf_congr

Modification history

2026-03-20 14:17
Mathlib/Order/CompleteLattice/Basic.lean
chore: use @[to_dual] extensively in CompleteLattice (#35209) …
Deleted Set.BijOn.iInf_congrView on Github →
2026-01-19 08:37
Mathlib/Order/CompleteLattice/Basic.lean
feat: lemmas to change variables in iSup / iInf / iUnion / iInter over a set (#33844) …
Added Set.BijOn.iInf_congrView on Github →