Basic results on multisets #
Produces a list of the elements in the multiset using choice.
Equations
Instances For
Induction principles #
@[irreducible]
def
Multiset.strongDownwardInduction
{α : Type u_1}
{p : Multiset α → Sort u_3}
{n : ℕ}
(H : (t₁ : Multiset α) → ({t₂ : Multiset α} → t₂.card ≤ n → t₁ < t₂ → p t₂) → t₁.card ≤ n → p t₁)
(s : Multiset α)
:
Suppose that, given that p t
can be defined on all supersets of s
of cardinality less than
n
, one knows how to define p s
. Then one can inductively define p s
for all multisets s
of
cardinality less than n
, starting from multisets of card n
and iterating. This
can be used either to define data, or to prove properties.
Equations
Instances For
theorem
Multiset.strongDownwardInduction_eq
{α : Type u_1}
{p : Multiset α → Sort u_3}
{n : ℕ}
(H : (t₁ : Multiset α) → ({t₂ : Multiset α} → t₂.card ≤ n → t₁ < t₂ → p t₂) → t₁.card ≤ n → p t₁)
(s : Multiset α)
:
strongDownwardInduction H s = H s fun {t₂ : Multiset α} (ht : t₂.card ≤ n) (_hst : s < t₂) => strongDownwardInduction H t₂ ht
def
Multiset.strongDownwardInductionOn
{α : Type u_1}
{p : Multiset α → Sort u_3}
{n : ℕ}
(s : Multiset α)
:
Analogue of strongDownwardInduction
with order of arguments swapped.
Equations
Instances For
theorem
Multiset.strongDownwardInductionOn_eq
{α : Type u_1}
{p : Multiset α → Sort u_3}
(s : Multiset α)
{n : ℕ}
(H : (t₁ : Multiset α) → ({t₂ : Multiset α} → t₂.card ≤ n → t₁ < t₂ → p t₂) → t₁.card ≤ n → p t₁)
:
(fun (a : s.card ≤ n) => s.strongDownwardInductionOn H a) = H s fun {t : Multiset α} (ht : t.card ≤ n) (_h : s < t) => t.strongDownwardInductionOn H ht
The equivalence between lists and multisets of a subsingleton type.
Equations
Instances For
@[simp]