le_union_right

Mathlib.Data.Multiset.UnionInter

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

English

t ≤ s ∪ t is always true.

Русский

Всегда верно t ≤ s ∪ t.

LaTeX

$$$ t \\le s \\cup t $$$

Lean4

theorem le_union_right : t ≤ s ∪ t :=
  le_add_left _ _

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

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

Разделы

Аффилиация

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