map_map

Mathlib.Data.Finset.Image

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

← MathLib Explorer

English

The map preserves strict subset: s.map f ⊂ t.map f iff s ⊂ t.

Русский

Отображение сохраняет строгое вложение: s.map f ⊂ t.map f ⇔ s ⊂ t.

LaTeX

$$$s.map f \subset t.map f \iff s \subset t$$$

Lean4

theorem map_map (f : α ↪ β) (g : β ↪ γ) (s : Finset α) : (s.map f).map g = s.map (f.trans g) :=
  eq_of_veq <| by simp only [map_val, Multiset.map_map]; rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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