eq_of_mk_mem — Mathlib

English

If both ⟨a,b⟩ and ⟨a,b'⟩ belong to a NodupKeys list, then b = b'.

Русский

Если в список NodupKeys входят элементы ⟨a,b⟩ и ⟨a,b'⟩, то b = b'.

LaTeX

$$$ \\mathrm{NodupKeys}(l) \\land (\\langle a,b\\rangle \\in l) \\land (\\langle a,b'\\rangle \\in l) \\implies b = b' $$$

Lean4

theorem eq_of_mk_mem {a : α} {b b' : β a} {l : List (Sigma β)} (nd : NodupKeys l) (h : Sigma.mk a b ∈ l)
    (h' : Sigma.mk a b' ∈ l) : b = b' := by grind [NodupKeys.eq_of_fst_eq]

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