preimage_empty_right

Mathlib.Data.Rel

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

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem preimage_empty_right : preimage R ∅ = ∅ := by aesop

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

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

Разделы

Аффилиация

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