image_preimage_val

Mathlib.Data.Set.Image

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

English

The same as coe_image_coe just with explicit val.

Русский

То же самое, но с явным Subtype.val.

LaTeX

$$$ \operatorname{image}(\operatorname{Subtype.val}, \operatorname{preimage}(\operatorname{Subtype.val}, t)) = s \cap t $$$

Lean4

theorem image_preimage_val (s t : Set α) : (Subtype.val : s → α) '' (Subtype.val ⁻¹' t) = s ∩ t :=
  image_preimage_coe s t

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

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

Разделы

Аффилиация

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