image_val_diff

Mathlib.Data.Set.Subset

URI: https://scilib.ai/kg/mathlib#Set.image_val_diff

← MathLib Explorer

English

The image of D \\ E equals image(D) \\ image(E).

Русский

Образ D \\ E равен образу D минус образ E.

LaTeX

$$$\\operatorname{image}(\\operatorname{val})(D \\setminus E) = \\operatorname{image}(\\operatorname{val}) D \\setminus \\operatorname{image}(\\operatorname{val}) E$$$

Lean4

@[simp]
theorem image_val_diff : (↑(D \ E) : Set α) = ↑D \ ↑E :=
  image_diff Subtype.val_injective _ _

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

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

Разделы

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

Аффилиация

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