image_empty_right

Mathlib.Data.Rel

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

English

For any relation R, the image of the empty set is empty: image R ∅ = ∅.

Русский

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

LaTeX

$$$\\forall (R : SetRel \\alpha \\beta), \\ image\,R\\,\\varnothing = \\varnothing$$$

Lean4

@[simp]
theorem image_empty_right : image R ∅ = ∅ := by aesop

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

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

Разделы

Аффилиация

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