image_empty_left

Mathlib.Data.Rel

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

English

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

Русский

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

LaTeX

$$$\\forall (s : Set \\alpha),\\\\ image (\\emptyset : SetRel \\alpha \\beta)\\,s = \\emptyset$$$

Lean4

@[simp]
theorem image_empty_left : image (∅ : SetRel α β) s = ∅ := by aesop

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

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

Разделы

Аффилиация

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