toFinset_surj_on

Mathlib.Data.Finset.Dedup

URI: https://scilib.ai/kg/mathlib#List.toFinset_surj_on

English

The function toFinset: List α → Finset α is surjective.

Русский

Функция toFinset: List α → Finset α сюрьективна.

LaTeX

$$$\\text{Surjective}(\\mathrm{toFinset} : \\mathsf{List}\\,\\alpha \\to \\mathsf{Finset}\\,\\alpha)$$$

Lean4

theorem toFinset_surj_on : Set.SurjOn toFinset {l : List α | l.Nodup} Set.univ :=
  by
  rintro ⟨⟨l⟩, hl⟩ _
  exact ⟨l, hl, (toFinset_eq hl).symm⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru