sym_singleton — Mathlib

English

The sym2 of a singleton equals the singleton of the replicated element.

Русский

Sym2 от единичного множества равен единичному набору повторённого элемента.

LaTeX

$$({a} : Finset α).sym n = {Sym.replicate n a}$$

Lean4

@[simp]
theorem sym_singleton (a : α) (n : ℕ) : ({ a } : Finset α).sym n = {Sym.replicate n a} :=
  eq_singleton_iff_unique_mem.2
    ⟨replicate_mem_sym (mem_singleton.2 rfl) _, fun _s hs ↦
      Sym.eq_replicate_iff.2 fun _b hb ↦ eq_of_mem_singleton <| mem_sym_iff.1 hs _ hb⟩

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