range_val_subtype

Mathlib.Data.Set.Image

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

English

The range of Subtype.val from Subtype p to α equals {x | p x}.

Русский

Образ Subtype.val из Subtype p в α равен {x | p x}.

LaTeX

$$$ \operatorname{range}(\operatorname{Subtype.val}) = \{ x \mid p x \} $$$

Lean4

theorem range_val_subtype {p : α → Prop} : range (Subtype.val : Subtype p → α) = {x | p x} :=
  range_coe

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

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

Разделы

Аффилиация

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