Theorems · Theorem · logic and foundations
Ordinal.opow_log_le_self
∀ (b : Ordinal.{u_1}) {x : Ordinal.{u_1}}, x ≠ 0 → b ^ Ordinal.log b x ≤ x- Defined in
- Mathlib.SetTheory.Ordinal.Exponential
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 88 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- le_reflproof · cited by 2,061
- Ordinalstatement and proof · cited by 1,688
- le_or_gtproof · cited by 269
- Ordinal.logstatement and proof · cited by 45
- Ordinal.opow_zeroproof · cited by 38
- Order.one_le_iff_ne_zeroproof · cited by 32
- Ordinal.log_of_left_le_oneproof · cited by 13
- Order.le_one_iffproof · cited by 10
- Ordinal.opow_le_iff_le_logproof · cited by 8
Cited by11
Results whose statement or proof uses this declaration.
- Ordinal.isPrincipal_add_iff_zero_or_omega0_opowproof · cited by 3
- Ordinal.div_opow_log_posproof · cited by 2
- Ordinal.log_eq_iffproof · cited by 2
- Ordinal.log_opow_mul_addproof · cited by 2
- Ordinal.sub_omega0_opow_log_ltproof · cited by 1
- Ordinal.log_mono_rightproof · cited by 1
- Ordinal.mod_opow_log_lt_selfproof · cited by 1
- Ordinal.isLeast_sub_lt_omega0_opow_logproof · cited by 0
- Ordinal.mul_eq_opow_log_succproof · cited by 0
- Ordinal.log_le_selfproof · cited by 0
- Ordinal.add_log_le_log_mulproof · cited by 0