pow_right_strictMono — Mathlib

English

Under suitable infinitude conditions, the map n ↦ X^n is strictly increasing in size as n grows.

Русский

При подходящих условиях бесконечности кардинальность степеней множества растёт строго с ростом n.

LaTeX

$$$X \subseteq G,\; 1\in X,\; X\text{ Nontrivial},\; (\overline{X})\text{ Infinite} \Rightarrow X^n < X^{n+1} \quad \text{for all } n$$$

Lean4

@[to_additive]
theorem pow_right_strictMono (hX₁ : 1 ∈ X) (hXclosure : (closure (X : Set G) : Set G).Infinite) :
    StrictMono fun n ↦ X ^ n := by
  obtain rfl | hX := eq_singleton_or_nontrivial hX₁
  · simp [closure_singleton_one] at hXclosure
  have h n : (X ^ (n - 1) : Set G) ≠ closure (X : Set G) := fun h ↦ by simp [← h, ← coe_pow] at hXclosure
  simpa [h] using pow_right_strictMonoOn hX₁ hX

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