union_le_iff

Mathlib.Data.Multiset.UnionInter

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

English

s ∪ t ≤ u if and only if s ≤ u and t ≤ u.

Русский

s ∪ t ≤ u ⇔ s ≤ u и t ≤ u.

LaTeX

$$$s \\cup t \\le u \\iff (s \\le u) \\land (t \\le u).$$$

Lean4

@[simp]
theorem union_le_iff : s ∪ t ≤ u ↔ s ≤ u ∧ t ≤ u :=
  sup_le_iff

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

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

Разделы

Аффилиация

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