isBounded_pow — Mathlib

English

For any s bounded and any natural n, the set of n-th powers of elements of s is bounded.

Русский

Для любого ограниченного множества s и любого натурального n множество элементов вида x^n, где x ∈ s, ограничено.

LaTeX

$$$\forall s\subseteq R\, (s\text{ bounded})\;\forall n\in\mathbb{N},\ IsBounded(\operatorname{image}(\lambda x. x^n)\,s)$$$

Lean4

@[to_additive]
theorem isBounded_pow {R : Type*} [Bornology R] [Monoid R] [BoundedMul R] {s : Set R} (s_bdd : Bornology.IsBounded s)
    (n : ℕ) : Bornology.IsBounded ((fun x ↦ x ^ n) '' s) := by
  induction n with
  | zero =>
    by_cases s_empty : s = ∅
    · simp [s_empty]
    simp_rw [← nonempty_iff_ne_empty] at s_empty
    simp [s_empty]
  | succ n
    hn =>
    have obs : ((fun x ↦ x ^ (n + 1)) '' s) ⊆ ((fun x ↦ x ^ n) '' s) * s :=
      by
      intro x hx
      simp only [mem_image] at hx
      obtain ⟨y, y_in_s, ypow_eq_x⟩ := hx
      rw [← ypow_eq_x, pow_succ y n]
      apply Set.mul_mem_mul _ y_in_s
      use y
    exact (isBounded_mul hn s_bdd).subset obs

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