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)
674theorem embed_le_iff_of_one_lt (γ : Generator) (hγ : 1 < γ.value) (a b : LogicNat) :
675 embed γ a ≤ embed γ b ↔ a ≤ b := by
proof body
Term-mode proof.
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)**. -/
depends on (8)
Lean names referenced from this declaration's body.
-
embed
in IndisputableMonolith.Foundation.ArithmeticFromLogic
decl_use
-
embed_eq_pow
in IndisputableMonolith.Foundation.ArithmeticFromLogic
decl_use
-
Generator
in IndisputableMonolith.Foundation.ArithmeticFromLogic
decl_use
-
LogicNat
in IndisputableMonolith.Foundation.ArithmeticFromLogic
decl_use
-
pow_le_pow_iff_of_one_lt
in IndisputableMonolith.Foundation.ArithmeticFromLogic
decl_use
-
toNat_le
in IndisputableMonolith.Foundation.ArithmeticFromLogic
decl_use
-
embed
in IndisputableMonolith.Foundation.HamiltonianEmergence
decl_use
-
value
in IndisputableMonolith.QFT.SpinStatistics
decl_use