image_val_compl

Mathlib.Data.Set.Subset

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

English

The image of the complement Dᶜ equals A \\ image(D).

Русский

Образ дополнения Dᶜ равен A \\ образ D.

LaTeX

$$$\\operatorname{image}(\\operatorname{val})(D^{c}) = A \\setminus \\operatorname{image}(\\operatorname{val}) D$$$

Lean4

@[simp]
theorem image_val_compl : ↑(Dᶜ) = A \ ↑D := by
  rw [compl_eq_univ_diff, image_val_diff, image_univ, Subtype.range_coe_subtype, setOf_mem_eq]

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

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

Разделы

Аффилиация

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