card_pow_mono — Mathlib

English

For arbitrary indices m ≤ n, if m ≠ 0, then #(s^m) ≤ #(s^n).

Русский

Для каких-либо m ≤ n, если m ≠ 0, то #(s^m) ≤ #(s^n).

LaTeX

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

Lean4

/-- See `Finset.Nonempty.card_pow_mono` for a version that works for zero powers. -/
@[to_additive /-- See `Finset.Nonempty.card_nsmul_mono` for a version that works for zero scalars. -/
    ]
theorem card_pow_mono (hm : m ≠ 0) (hmn : m ≤ n) : #(s ^ m) ≤ #(s ^ n) :=
  by
  obtain rfl | hs := s.eq_empty_or_nonempty
  · simp [hm]
  · exact hs.card_pow_mono hmn

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