eq_of_fst_le_fst_of_snd_le_snd — Mathlib

English

Under monotone order assumptions (IsCancelMul, MulLeftMono, MulRightStrictMono) if x.fst ≤ y.fst and x.snd ≤ y.snd for x,y in the MulAntidiagonal, then x = y.

Русский

При заданных условиях монотонности, если первая координата x≤ y и вторая x≤ y, то x = y.

LaTeX

$$For x,y ∈ (s.mulAntidiagonal t a).Elem, if x.val.fst ≤ y.val.fst and x.val.snd ≤ y.val.snd, then x = y.$$

Lean4

@[to_additive Set.AddAntidiagonal.eq_of_fst_le_fst_of_snd_le_snd]
theorem eq_of_fst_le_fst_of_snd_le_snd (h₁ : (x : α × α).1 ≤ (y : α × α).1) (h₂ : (x : α × α).2 ≤ (y : α × α).2) :
    x = y :=
  eq_of_fst_eq_fst <|
    h₁.eq_of_not_lt fun hlt =>
      (mul_lt_mul_of_lt_of_le hlt h₂).ne <| (mem_mulAntidiagonal.1 x.2).2.2.trans (mem_mulAntidiagonal.1 y.2).2.2.symm

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