cons_subset_cons

Mathlib.Data.Multiset.ZeroCons

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

English

For all a, s, t, a ::ₘ s ⊆ t iff a ∈ t and s ⊆ t.

Русский

Для всех a, s, t: a ::ₘ s ⊆ t эквивалентно a ∈ t и s ⊆ t.

LaTeX

$$$\\forall {a:\\alpha} {s t:\\mathrm{Multiset}\\alpha},\\ a ::ₘ s \\subseteq t \\leftrightarrow (a \\in t \\land s \\subseteq t)$$$

Lean4

theorem cons_subset_cons {a : α} {s t : Multiset α} : s ⊆ t → a ::ₘ s ⊆ a ::ₘ t :=
  Quotient.inductionOn₂ s t fun _ _ => List.cons_subset_cons _

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

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

Разделы

Аффилиация

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