powerset_injective

Mathlib.Data.Finset.Powerset

URI: https://scilib.ai/kg/mathlib#Finset.powerset_injective

English

The map s ↦ powerset(s) is injective on Finset α.

Русский

Отображение s → powerset(s) инъективно на Finset α.

LaTeX

$$$$\\text{Injective}(\\text{powerset} : \\text{Finset } \\alpha \\to \\text{Finset}(\\text{Finset } \\alpha)).$$$$

Lean4

theorem powerset_injective : Injective (powerset : Finset α → Finset (Finset α)) :=
  (injective_of_le_imp_le _) powerset_mono.1

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

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

Разделы

Аффилиация

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