Theorem Function.update_inf

Modification history

2025-12-24 12:03
Mathlib/Order/Lattice.lean
feat(Order/Lattice): use `@[to_dual]` (#33142) …
Deleted Function.update_infView on Github →
2023-05-01 15:10
Mathlib/Order/Lattice.lean
feat: `f.update i '' Icc a b = Icc (f.update i a) (f.update i b)` (#3747) …
Added Function.update_infView on Github →