pith. machine review for the scientific record. sign in
theorem proved term proof

pow_lt_pow_iff_of_one_lt

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 662private theorem pow_lt_pow_iff_of_one_lt {γ : ℝ} (hγ : 1 < γ) (n m : Nat) :
 663    γ ^ n < γ ^ m ↔ n < m := by

proof body

Term-mode proof.

 664  constructor
 665  · intro h
 666    by_contra hle
 667    push_neg at hle
 668    have := pow_le_pow_right₀ (le_of_lt hγ) hle
 669    linarith
 670  · intro h
 671    exact pow_lt_pow_right₀ hγ h
 672
 673/-- **Embedding monotonicity (γ > 1)**: the embedding is order-preserving. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (4)

Lean names referenced from this declaration's body.