antidiagonal_subtype_ext — Mathlib

English

Extending along the subtype of antidiagonal preserves the equality: two elements of the subtype with the same first coordinate are equal.

Русский

Расширение по подтипу антидиагонали сохраняет равенство: два элемента подтипа с одной и той же первой координатой равны.

LaTeX

$$$p=q \\iff p.id.\\text{val}.1 = q.id.\\text{val}.1 \\quad (p,q \\in \\operatorname{antidiagonal}(n))$$$

Lean4

/-- A point in the antidiagonal is determined by its first co-ordinate (subtype version of
`Finset.antidiagonal_congr`). This lemma is used by the `ext` tactic. -/
@[ext]
theorem antidiagonal_subtype_ext {p q : antidiagonal n} (h : p.val.1 = q.val.1) : p = q :=
  Subtype.ext ((antidiagonal_congr p.prop q.prop).mpr h)

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