mem_powerset

Mathlib.Data.Multiset.Powerset

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

English

For any multisets s, t, s ∈ powerset t if and only if s ≤ t.

Русский

Для любых мультимножеств s, t верно: s ∈ powerset(t) тогда и только тогда, когда s ≤ t.

LaTeX

$$$ {s,t : Multiset\\alpha} \\; s \\in \\mathrm{powerset}(t) \\iff s \\le t $$$

Lean4

@[simp]
theorem mem_powerset {s t : Multiset α} : s ∈ powerset t ↔ s ≤ t :=
  Quotient.inductionOn₂ s t <| by simp [Subperm, and_comm]

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

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

Разделы

Аффилиация

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