rel_zero_left

Mathlib.Data.Multiset.ZeroCons

URI: https://scilib.ai/kg/mathlib#Multiset.rel_zero_left

English

For any relation r, Rel r 0 b is equivalent to b = 0.

Русский

Для любой связи r, Rel r 0 b эквивалентно b = 0.

LaTeX

$$$Rel(r)\ 0\ b \iff b = 0$$$

Lean4

@[simp]
theorem rel_zero_left {b : Multiset β} : Rel r 0 b ↔ b = 0 := by rw [rel_iff]; simp

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

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

Разделы

Аффилиация

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