range_coe

Mathlib.Data.Set.Image

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

English

The image of the set s under the inclusion from s to α is s itself.

Русский

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

LaTeX

$$$ \operatorname{range}((\uparrow) : s \to \alpha) = s $$$

Lean4

theorem range_coe {s : Set α} : range ((↑) : s → α) = s :=
  by
  rw [← image_univ]
  simp [-image_univ, coe_image]

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

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

Разделы

Аффилиация

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