mem_cons

Mathlib.Data.Multiset.ZeroCons

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

English

For a,b,s, a ∈ b ::ₘ s iff a = b or a ∈ s.

Русский

Для произвольных a, b и s, a ∈ b ::ₘ s эквивалентно a = b или a ∈ s.

LaTeX

$$$a \\in b ::ₘ s \\iff a = b \\lor a \\in s$$$

Lean4

@[simp, grind =]
theorem mem_cons {a b : α} {s : Multiset α} : a ∈ b ::ₘ s ↔ a = b ∨ a ∈ s :=
  Quot.inductionOn s fun _ => List.mem_cons

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

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

Разделы

Аффилиация

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