pow_le_pow_iff_of_one_lt

formal source

 647of the abstract Peano order from Section 5b. -/
 648
 649/-- For `γ > 1`, `γⁿ ≤ γᵐ ↔ n ≤ m` on `Nat`. -/
 650private theorem pow_le_pow_iff_of_one_lt {γ : ℝ} (hγ : 1 < γ) (n m : Nat) :
 651    γ ^ n ≤ γ ^ m ↔ n ≤ m := by
 652  constructor
 653  · intro h
 654    by_contra hlt
 655    push_neg at hlt
 656    have : γ ^ m < γ ^ n := pow_lt_pow_right₀ hγ hlt
 657    linarith
 658  · intro h
 659    exact pow_le_pow_right₀ (le_of_lt hγ) h
 660
 661/-- For `γ > 1`, `γⁿ < γᵐ ↔ n < m` on `Nat`. -/
 662private theorem pow_lt_pow_iff_of_one_lt {γ : ℝ} (hγ : 1 < γ) (n m : Nat) :
 663    γ ^ n < γ ^ m ↔ n < m := by
 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. -/
 674theorem embed_le_iff_of_one_lt (γ : Generator) (hγ : 1 < γ.value) (a b : LogicNat) :
 675    embed γ a ≤ embed γ b ↔ a ≤ b := by
 676  rw [embed_eq_pow, embed_eq_pow, pow_le_pow_iff_of_one_lt hγ, ← LogicNat.toNat_le]
 677
 678/-- **Embedding strict monotonicity (γ > 1)**. -/
 679theorem embed_lt_iff_of_one_lt (γ : Generator) (hγ : 1 < γ.value) (a b : LogicNat) :
 680    embed γ a < embed γ b ↔ a < b := by