card_pow_mono — Mathlib

English

If s is nonempty, the map n ↦ #(s^n) is monotone on natural numbers.

Русский

Если S непусто, то отображение n ↦ #(S^n) монотонно на натуральных числах.

LaTeX

$$$$ s \neq \varnothing \Rightarrow \forall n,m \in \mathbb{N},\; n \le m \Rightarrow #(s^n) \le #(s^m). $$$$

Lean4

/-- See `Finset.card_pow_mono` for a version that works for the empty set. -/
@[to_additive /-- See `Finset.card_nsmul_mono` for a version that works for the empty set. -/
    ]
protected theorem card_pow_mono (hs : s.Nonempty) : Monotone fun n : ℕ ↦ #(s ^ n) :=
  monotone_nat_of_le_succ fun n ↦ by rw [pow_succ]; exact card_le_card_mul_right hs

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