inter_dom_subset_preimage_image

Mathlib.Data.Rel

URI: https://scilib.ai/kg/mathlib#SetRel.inter_dom_subset_preimage_image

English

s ∩ dom(R) ⊆ preimage (image R s).

Русский

Пересечение s с доменом R содержится в предобразе образа s через R.

LaTeX

$$$\\forall (s : Set \\alpha),\\\\ s \\cap R.dom \\subseteq R.preimage (R.image s)$$$

Lean4

theorem inter_dom_subset_preimage_image : s ∩ R.dom ⊆ R.preimage (image R s) := by aesop (add simp [Set.subset_def])

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

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

Разделы

Аффилиация

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