Theorems · Theorem · logic and foundations
Ordinal.opow_le_opow_left
∀ {a b : Ordinal.{u_1}} (c : Ordinal.{u_1}), a ≤ b → a ^ c ≤ b ^ c- Defined in
- Mathlib.SetTheory.Ordinal.Exponential
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 89 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- LE.le.transproof · cited by 3,151
- LT.lt.leproof · cited by 2,189
- Ordinalstatement and proof · cited by 1,688
- LT.lt.trans_leproof · cited by 678
- mul_le_mul'proof · cited by 274
- Order.IsSuccLimitproof · cited by 255
- pos_iff_ne_zeroproof · cited by 180
- Ordinal.opow_zeroproof · cited by 38
- Ordinal.limitRecOnproof · cited by 20
- Ordinal.zero_opowproof · cited by 13
- Ordinal.opow_add_oneproof · cited by 9
- Ordinal.opow_le_of_isSuccLimitproof · cited by 7
Cited by4
Results whose statement or proof uses this declaration.
- Ordinal.opow_le_opowproof · cited by 3
- Ordinal.card_opow_le_of_omega0_le_rightproof · cited by 2
- ONote.repr_opow_aux₁proof · cited by 1
- Ordinal.opow_lt_opow_left_of_succproof · cited by 0