coe_map_subset_range

Mathlib.Data.Finset.Image

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

English

The set underlying the image Finset s.map f equals the image of s.toSet under f.

Русский

Множество под образованием Finset.map равно образу множества s под f.

LaTeX

$$$ (s.map f : Set \beta) = f '' s $$$

Lean4

theorem coe_map_subset_range (f : α ↪ β) (s : Finset α) : (s.map f : Set β) ⊆ Set.range f := by grind

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

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

Разделы

Аффилиация

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