powersetCard_mono — Mathlib

English

If s ≤ t then powersetCard n s ≤ powersetCard n t for any n.

Русский

Если s ≤ t, то для любого n выполняется powersetCard n s ≤ powersetCard n t.

LaTeX

$$$s \le t \Rightarrow \mathrm{powersetCard}(n,s) \le \mathrm{powersetCard}(n,t)$$$

Lean4

theorem powersetCard_mono (n : ℕ) {s t : Multiset α} (h : s ≤ t) : powersetCard n s ≤ powersetCard n t :=
  leInductionOn h fun {l₁ l₂} h => by
    simp only [powersetCard_coe, coe_le]
    exact ((sublistsLen_sublist_of_sublist _ h).map _).subperm

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