Theorem sup_eq_inf

Modification history

2025-12-24 12:03
Mathlib/Order/Lattice.lean
feat(Order/Lattice): use `@[to_dual]` (#33142) …
Deleted sup_eq_infView on Github →
2023-01-06 20:48
Mathlib/Order/Lattice.lean
feat: `a ⊔ b = a ⊓ b ↔ a = b` (#1078) …
Added sup_eq_infView on Github →