exists_lt_pow_of_lt_one — Mathlib

English

If x < 1 in a densely ordered monoid with the appropriate structure, then for every n there exists y < 1 with x < y^n.

Русский

Если x < 1 в плотном упорядоченном моноиде с необходимой структурой, то для каждого n существует y < 1 такой, что x < y^n.

LaTeX

$$$x < 1 \rightarrow \forall n \in \mathbb{N},\exists y<1,\ x < y^n$$$

Lean4

@[to_additive]
theorem exists_lt_pow_of_lt_one (hx : x < 1) (n : ℕ) : ∃ y : M, y < 1 ∧ x < y ^ n :=
  by
  obtain ⟨y, hy, hy'⟩ := exists_pow_lt_of_one_lt (one_lt_inv_of_inv hx) n
  use y⁻¹, inv_lt_one_of_one_lt hy
  simpa [lt_inv'] using hy'

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