eq_of_fst_le_fst_of_snd_le_snd — Mathlib

English

If the first coordinates are ordered and the second coordinates are ordered, then the two elements of smulAntidiagonal are equal.

Русский

Если первые координаты упорядочены и вторые координаты упорядочены, то элементы smulAntidiagonal равны.

LaTeX

$$$\forall x,y \in (s.smulAntidiagonal t a).Elem,\; x.fst \le y.fst \rightarrow x.snd \le y.snd \\Rightarrow x = y$$$

Lean4

@[to_additive VAddAntidiagonal.eq_of_fst_le_fst_of_snd_le_snd]
theorem eq_of_fst_le_fst_of_snd_le_snd (h₁ : (x : G × P).1 ≤ (y : G × P).1) (h₂ : (x : G × P).2 ≤ (y : G × P).2) :
    x = y :=
  eq_of_fst_eq_fst <|
    h₁.eq_of_not_lt fun hlt =>
      (smul_lt_smul_of_lt_of_le hlt h₂).ne <|
        (mem_smulAntidiagonal.1 x.2).2.2.trans (mem_smulAntidiagonal.1 y.2).2.2.symm

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