English
For any a,b,c in a lattice, the pair of equalities a ∧ b = c and a ∨ b = c holds iff a = c and b = c.
Русский
Для любых a, b, c в решётке равны одновременно a ∧ b = c и a ∨ b = c тогда и только тогда, когда a = c и b = c.
LaTeX
$$$ (a \wedge b = c) \wedge (a \vee b = c) \iff (a = c) \wedge (b = c)$$$
Lean4
theorem inf_eq_and_sup_eq_iff : a ⊓ b = c ∧ a ⊔ b = c ↔ a = c ∧ b = c :=
by
refine ⟨fun h ↦ ?_, ?_⟩
· obtain rfl := sup_eq_inf.1 (h.2.trans h.1.symm)
simpa using h
· rintro ⟨rfl, rfl⟩
exact ⟨inf_idem _, sup_idem _⟩