English
There is a canonical equivalence between α and Sym α 1 given by a ↦ {a}.
Русский
Существует каноническое эквивалентное отображение между α и Sym α 1, задаваемое a ↦ {a}.
LaTeX
$$$\\alpha \\cong \\mathrm{Sym}(\\alpha, 1)$ with $a \\mapsto \\{a\\}$ as the forward map and an explicit inverse.$$
Lean4
/-- `a ↦ {a}` as an equivalence between `α` and `Sym α 1`. -/
@[simps apply]
def oneEquiv : α ≃ Sym α 1 where
toFun a := ⟨{ a }, by simp⟩
invFun
s :=
(Equiv.subtypeQuotientEquivQuotientSubtype (·.length = 1) _ (fun _ ↦ Iff.rfl) (fun l l' ↦ by rfl) s).liftOn
(fun l ↦ l.1.head <| List.length_pos_iff.mp <| by simp) fun ⟨_, _⟩ ⟨_, h⟩ ↦ fun perm ↦
by
obtain ⟨a, rfl⟩ := List.length_eq_one_iff.mp h
exact List.eq_of_mem_singleton (perm.mem_iff.mp <| List.head_mem _)
right_inv := by rintro ⟨⟨l⟩, h⟩; obtain ⟨a, rfl⟩ := List.length_eq_one_iff.mp h; rfl
