coe_image_univ

Mathlib.Data.Set.Image

URI: https://scilib.ai/kg/mathlib#Subtype.coe_image_univ

English

The image of the universal set under the inclusion equals s.

Русский

Образ все множества под включением равен s.

LaTeX

$$$ (\uparrow) '' \mathrm{Set.univ} = s $$$

Lean4

theorem coe_image_univ (s : Set α) : ((↑) : s → α) '' Set.univ = s :=
  image_univ.trans range_coe

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

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

Разделы

Аффилиация

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