eq_of_inf_eq_sup_eq — Mathlib

English

If b ∧ a = c ∧ a and b ∨ a = c ∨ a, then b = c.

Русский

Если b ∧ a = c ∧ a и b ∨ a = c ∨ a, то b = c.

LaTeX

$$$\text{If } b \wedge a = c \wedge a \text{ and } b \vee a = c \vee a, \text{ then } b = c$$$

Lean4

theorem eq_of_inf_eq_sup_eq {a b c : α} (h₁ : b ⊓ a = c ⊓ a) (h₂ : b ⊔ a = c ⊔ a) : b = c :=
  le_antisymm (le_of_inf_le_sup_le (le_of_eq h₁) (le_of_eq h₂))
    (le_of_inf_le_sup_le (le_of_eq h₁.symm) (le_of_eq h₂.symm))

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