mem_powersetCard — Mathlib

English

A submultiset s belongs to powersetCard n t exactly when s is a submultiset of t and s has size n.

Русский

Подмножество s принадлежит powersetCard n t тогда и только тогда, когда s является подмножество t и имеет размер n.

LaTeX

$$$s \in \mathrm{powersetCard} n t \;\iff\; s \le t \land \mathrm{card}(s) = n$$$

Lean4

@[simp]
theorem mem_powersetCard {n : ℕ} {s t : Multiset α} : s ∈ powersetCard n t ↔ s ≤ t ∧ card s = n :=
  Quotient.inductionOn t fun l => by simp [powersetCard_coe']

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