coe_image_subset_range

Mathlib.Data.Finset.Image

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

← MathLib Explorer

English

The image s of f is contained in the range of f when viewed as a set.

Русский

Образ s под действием f по отношению к множеству содержится в диапазоне f.

LaTeX

$$$\mathrm{image}\ f\ s \subseteq \mathrm{range}\ f$$$

Lean4

theorem coe_image_subset_range : ↑(s.image f) ⊆ Set.range f :=
  calc
    ↑(s.image f) = f '' ↑s := coe_image
    _ ⊆ Set.range f := Set.image_subset_range f ↑s

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

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

Разделы

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

Аффилиация

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