map_inj

Mathlib.Data.Finset.Image

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

English

For Finsets s1 and s2, map f is injective: s1.map f = s2.map f implies s1 = s2.

Русский

Для Finset s1, s2 отображение map f инъективно: равны их образы — сами множества.

LaTeX

$$$s_1.map f = s_2.map f \iff s_1 = s_2$$$

Lean4

@[simp]
theorem map_inj {s₁ s₂ : Finset α} : s₁.map f = s₂.map f ↔ s₁ = s₂ :=
  (mapEmbedding f).injective.eq_iff

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

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

Разделы

Аффилиация

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