mk_cons — Mathlib

English

A Finset built from a Multiset of the form ⟨a ::ₘ s, h⟩ equals cons a ⟨s, (nodup_cons.1 h).2⟩ (nodup_cons.1 h).1 when appropriate nodup is given.

Русский

Финсет, построенный из мультисета вида ⟨a ::ₘ s, h⟩, равен cons a ⟨s, (nodup_cons.1 h).2⟩ (nodup_cons.1 h).1 при заданном nodup.

LaTeX

$$$([s : Multiset α] (h : (a ::ₘ s).Nodup)) \rightarrow (⟨a ::ₘ s, h⟩ : Finset α) = cons a ⟨s, (nodup_cons.1 h).2⟩ (nodup_cons.1 h).1$$$

Lean4

@[simp]
theorem mk_cons {s : Multiset α} (h : (a ::ₘ s).Nodup) :
    (⟨a ::ₘ s, h⟩ : Finset α) = cons a ⟨s, (nodup_cons.1 h).2⟩ (nodup_cons.1 h).1 :=
  rfl

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