sigma_sub_ext — Mathlib

English

If the tails of two Sigma elements are equal as multisets, the entire elements are equal.

Русский

Если хвосты двух элементов в выписке совпадают как множества, то сами элементы равны.

LaTeX

$$$ m_1 = m_2 \\;\\text{ если } m_1.2 = m_2.2 \\text{ как множества}$$$

Lean4

theorem sigma_sub_ext {m₁ m₂ : Σ i : Fin (n + 1), Sym α (n - i)} (h : (m₁.2 : Multiset α) = m₂.2) : m₁ = m₂ :=
  Sigma.subtype_ext
    (Fin.ext <| by
      rw [← Nat.sub_sub_self (Nat.le_of_lt_succ m₁.1.is_lt), ← m₁.2.2, val_eq_coe, h, ← val_eq_coe, m₂.2.2,
        Nat.sub_sub_self (Nat.le_of_lt_succ m₂.1.is_lt)])
    h

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