inf_eq_inf_and_sup_eq_sup — Mathlib

English

In a linear order, two Sym2 elements are equal if and only if their infima and suprema agree.

Русский

В линейном порядке равны два элемента Sym2 тогда и только тогда, когда совпадают их Inf и Sup.

LaTeX

$$$s.\inf = t.\inf \land s.\sup = t.\sup \iff s = t$$$

Lean4

/-- In a linear order, two symmetric squares are equal if and only if
they have the same infimum and supremum. -/
theorem inf_eq_inf_and_sup_eq_sup [LinearOrder α] {s t : Sym2 α} : s.inf = t.inf ∧ s.sup = t.sup ↔ s = t :=
  by
  induction s with
  | _ a b
  induction t with
  | _ c d
  obtain hab | hba := le_total a b <;> obtain hcd | hdc := le_total c d <;> aesop (add unsafe le_antisymm)

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