inter_cod_subset_image_preimage

Mathlib.Data.Rel

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

English

t ∩ cod(R) ⊆ image R (R.preimage t).

Русский

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

LaTeX

$$$\\forall (t : Set \\beta),\\\\ t \\cap R.cod \\subseteq image R (R.preimage t)$$$

Lean4

theorem inter_cod_subset_image_preimage : t ∩ R.cod ⊆ image R (R.preimage t) := by aesop (add simp [Set.subset_def])

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

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

Разделы

Аффилиация

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