exists_inv_two_pow_lt — Mathlib

English

There exists n ∈ ℕ such that (2⁻¹)ⁿ < a for a ≠ ∞ and a ≠ 0.

Русский

Существует n ∈ ℕ такое, что (2⁻¹)ⁿ < a при a ≠ ∞ и a ≠ 0.

LaTeX

$$$\\exists n \\in \\mathbb{N},\\; (2^{-1})^{n} < a$$$

Lean4

theorem exists_inv_two_pow_lt (ha : a ≠ 0) : ∃ n : ℕ, 2⁻¹ ^ n < a :=
  by
  rcases exists_inv_nat_lt ha with ⟨n, hn⟩
  refine ⟨n, lt_trans ?_ hn⟩
  rw [← ENNReal.inv_pow, ENNReal.inv_lt_inv]
  norm_cast
  exact n.lt_two_pow_self

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