cons_subset

Mathlib.Data.Multiset.ZeroCons

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

English

If s ⊆ t then a ::ₘ s ⊆ a ::ₘ t.

Русский

Если s ⊆ t, то a ::ₘ s ⊆ a ::ₘ t.

LaTeX

$$$s \\subseteq t \\;\rightarrow\; a ::ₘ s \\subseteq a ::ₘ t$$$

Lean4

@[simp]
theorem cons_subset {a : α} {s t : Multiset α} : a ::ₘ s ⊆ t ↔ a ∈ t ∧ s ⊆ t := by simp [subset_iff, or_imp, forall_and]

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

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

Разделы

Аффилиация

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