mathlib3
d6aad952 - feat(order/lattice): `a ⊔ b = a ⊓ b ↔ a = b` (#17966)

Commit

2 years ago

feat(order/lattice): `a ⊔ b = a ⊓ b ↔ a = b` (#17966) and `a ⊓ b = c ∧ a ⊔ b = c ↔ a = c ∧ b = c`

Author

YaelDillies

Parents