sup_mono

Mathlib.Data.Multiset.Lattice

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

English

Let α be a semilattice with bottom. If s1 ⊆ s2, then s1.sup ≤ s2.sup.

Русский

Пусть α — полусортированное множество с нижним элементом. Если s1 ⊆ s2, то sup s1 ≤ sup s2.

LaTeX

$$$$ s_1 \\subseteq s_2 \\implies s_1.sup \\le s_2.sup $$$$

Lean4

@[gcongr]
theorem sup_mono {s₁ s₂ : Multiset α} (h : s₁ ⊆ s₂) : s₁.sup ≤ s₂.sup :=
  sup_le.2 fun _ hb => le_sup (h hb)

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

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

Разделы

Аффилиация

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