map_eq_of_subset

Mathlib.Data.Finset.Card

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

English

If s maps under f into s (i.e., s.map f ⊆ s) for an embedding f, then s.map f = s.

Русский

Если отображение f заменяет s подмножество s, то s.map f = s.

LaTeX

$$$\\forall {f : α \\hookrightarrow α},\\; (s.map f \\subseteq s) \\Rightarrow s.map f = s$$$

Lean4

theorem map_eq_of_subset {f : α ↪ α} (hs : s.map f ⊆ s) : s.map f = s :=
  eq_of_subset_of_card_le hs (card_map _).ge

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

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

Разделы

Аффилиация

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