Theorems · Theorem · order theory
WithBot.bot_lt_coe
∀ {α : Type u_1} [inst : LT α] (a : α), ⊥ < ↑a- Defined in
- Mathlib.Order.WithBot
- Cited by
- 37 results in Mathlib
- Foundations
- Depth 13 from the axioms · uses propext, Quot.sound
- Assumes
- LT
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Bot.botstatement and proof · cited by 4,720
- WithBotstatement · cited by 1,498
- WithBot.somestatement · cited by 541
Cited by37
Results whose statement or proof uses this declaration.
- Polynomial.coeff_eq_zero_of_natDegree_ltproof · cited by 55
- EReal.bot_lt_coeproof · cited by 13
- Polynomial.degree_lt_iff_coeff_zeroproof · cited by 5
- Finset.le_sup'_iffproof · cited by 5
- Lagrange.degree_interpolate_ltproof · cited by 4
- Polynomial.degree_sum_fin_ltproof · cited by 4
- Lagrange.sum_basisproof · cited by 3
- minpoly.mem_range_of_degree_eq_oneproof · cited by 3
- WithBot.image_coe_Icoproof · cited by 3
- Finset.sup'_lt_iffproof · cited by 2
- PowerSeries.isWeierstrassDivisionAt_zeroproof · cited by 2
- Order.krullDim_eq_topproof · cited by 2