Commit 2023-01-06 20:48 f7bf5792

View on Github →

feat: a ⊔ b = a ⊓ b ↔ a = b (#1078) Match https://github.com/leanprover-community/mathlib/pull/17966

Estimated changes

added theorem inf_eq_and_sup_eq_iff
added theorem inf_eq_sup
modified theorem inf_lt_sup
added theorem sup_eq_inf