union_le

Mathlib.Data.Multiset.UnionInter

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

English

If s ≤ u and t ≤ u for multisets s, t, u, then s ∪ t ≤ u.

Русский

Если s ≤ u и t ≤ u для мультимножества s, t, u, то s ∪ t ≤ u.

LaTeX

$$$\\forall s,t,u \\in \\mathrm{Multiset}(\\alpha),\\ (s \\le u) \\land (t \\le u) \\Rightarrow (s \\cup t) \\le u.$$$

Lean4

theorem union_le (h₁ : s ≤ u) (h₂ : t ≤ u) : s ∪ t ≤ u := by rw [← eq_union_left h₂]; exact union_le_union_right h₁ t

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

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

Разделы

Аффилиация

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