Theorems · Theorem · logic and foundations

Ordinal.opow_le_iff_le_log

∀ {b x c : Ordinal.{u_1}}, 1 < b → x ≠ 0 → (b ^ c ≤ x ↔ c ≤ Ordinal.log b x)

opow b and log b (almost) form a Galois connection. See opow_le_iff_le_log' for a variant assuming c ≠ 0 rather than x ≠ 0. See also le_log_of_opow_le and opow_le_of_le_log, which are both separate implications under weaker assumptions.

Defined in

Mathlib.SetTheory.Ordinal.Exponential

Cited by

8 results in Mathlib

Foundations

Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound