eq_of_fst_eq_fst — Mathlib

English

If two elements x,y of mulAntidiagonal have equal first coordinates, then x = y.

Русский

Если x и y из mulAntidiagonal s t a имеют одинаковые первые координаты, то x = y.

LaTeX

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

Lean4

@[to_additive Set.AddAntidiagonal.eq_of_fst_eq_fst]
theorem eq_of_fst_eq_fst (h : (x : α × α).fst = (y : α × α).fst) : x = y :=
  Subtype.ext <| Prod.ext h <| fst_eq_fst_iff_snd_eq_snd.1 h

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