preimage_empty_left

Mathlib.Data.Rel

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

English

The preimage of the empty relation on any set t is empty: preimage (∅ : SetRel α β) t = ∅.

Русский

Предобраз пустого отношения слева от множества t равен пустоте.

LaTeX

$$$\\forall (t : Set \\beta),\\\\ preimage (\\emptyset : SetRel \\alpha \\beta)\\,t = \\emptyset$$$

Lean4

@[simp]
theorem preimage_empty_left : preimage (∅ : SetRel α β) t = ∅ := by aesop

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

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

Разделы

Аффилиация

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