eq_of_fst_eq — Mathlib

English

If two elements s, s' of a NodupKeys list have the same first component, then s = s'.

Русский

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

LaTeX

$$$ l.NodupKeys \\Rightarrow \\forall s,s'\\in l,\\; s.1 = s'.1 \\Rightarrow s = s' $$$

Lean4

theorem eq_of_fst_eq {l : List (Sigma β)} (nd : NodupKeys l) {s s' : Sigma β} (h : s ∈ l) (h' : s' ∈ l) :
    s.1 = s'.1 → s = s' :=
  @Pairwise.forall_of_forall _ (fun s s' : Sigma β => s.1 = s'.1 → s = s') _ (fun _ _ H h => (H h.symm).symm)
    (fun _ _ _ => rfl) ((nodupKeys_iff_pairwise.1 nd).imp fun h h' => (h h').elim) _ h _ h'

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