Theorem inf_lt_sup

Modification history

2024-04-01 16:53
Mathlib/Order/Lattice.lean
chore: avoid Ne.def (adaptation for nightly-2024-03-27) (#11813)
Modified inf_lt_supView on Github →
2023-01-06 20:48
Mathlib/Order/Lattice.lean
feat: `a ⊔ b = a ⊓ b ↔ a = b` (#1078) …
Modified inf_lt_supView on Github →
2022-11-25 17:46
Mathlib/Order/Lattice.lean
feat: port Order.Lattice (#642) …
Added inf_lt_supView on Github →