Theorems · Theorem · order theory
one_pos
∀ {α : Type u_1} [inst : Zero α] [inst_1 : One α] [inst_2 : PartialOrder α] [ZeroLEOneClass α] [NeZero 1], 0 < 1Alias of zero_lt_one.
See zero_lt_one' for a version with the type explicit.
- Defined in
- Mathlib.Algebra.Order.ZeroLEOne
- Cited by
- 102 results in Mathlib
- Foundations
- Depth 8 from the axioms, rests on 27 definitions · uses no axioms
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.
- PartialOrderstatement · cited by 6,410
- zero_lt_oneproof · cited by 598
- ZeroLEOneClassstatement · cited by 304
Cited by102
Results whose statement or proof uses this declaration.
- exists_nat_geproof · cited by 20
- uniformity_basis_edistproof · cited by 17
- Absorbs.exists_posproof · cited by 8
- Asymptotics.isLittleOTVS_iff_isLittleOproof · cited by 7
- Metric.disjoint_nhds_coboundedproof · cited by 7
- NormedField.exists_norm_lt_oneproof · cited by 6
- interior_subset_gauge_lt_oneproof · cited by 5
- VectorFourier.hasFDerivAt_fourierIntegralproof · cited by 5
- isBoundedBilinearMap_smulproof · cited by 5
- Hyperreal.IsSt.not_infiniteproof · cited by 4
- LinearOrderedAddCommGroup.discrete_iff_not_denselyOrderedproof · cited by 4
- egauge_ball_le_of_one_lt_normproof · cited by 4