image_inj

Mathlib.Data.Finset.Image

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

English

For injective f, s.image f = t.image f iff s = t.

Русский

Для инъективной f равенство образов вернулось в равенство исходных множеств: s.image f = t.image f ⇔ s = t.

LaTeX

$$$\text{Injective } f \Rightarrow (s.image f = t.image f) \iff (s = t)$$$

Lean4

theorem image_inj {t : Finset α} (hf : Injective f) : s.image f = t.image f ↔ s = t :=
  (image_injective hf).eq_iff

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

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

Разделы

Аффилиация

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