add_eq_union_right_of_le

Mathlib.Data.Multiset.UnionInter

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

← MathLib Explorer

English

If z ≤ y, then x + y = x ∪ z iff y = z ∧ Disjoint x y.

Русский

Пусть z ≤ y. Тогда x + y = x ∪ z эквивалентно y = z и Disjoint x y.

LaTeX

$$$z \\le y \\Rightarrow x + y = x \\cup z \\iff (y = z) \\land Disjoint x y$$$

Lean4

theorem add_eq_union_right_of_le [DecidableEq α] {x y z : Multiset α} (h : z ≤ y) :
    x + y = x ∪ z ↔ y = z ∧ Disjoint x y := by simpa only [and_comm] using add_eq_union_left_of_le h

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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