inf_eq_and_sup_eq_iff — Mathlib

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 _⟩

Похожие утверждения