Mathlib Map

Theorems · Theorem · general topology

unitInterval.le_one

∀ (x : ↑unitInterval), ↑x ≤ 1
Defined in
Mathlib.Topology.UnitInterval
Cited by
3 results in Mathlib
Foundations
Depth 103 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

bernsteinApproximation_uniform · cited by 1bernsteinApproximation_un…Path.Homotopy.transAssocReparamAux_mem_I · cited by 1Homotopy.transAssocRepara…unitInterval.qRight_one_left · cited by 0unitInterval.qRight_one_l…Set · cited by 53352SetReal · cited by 25697RealSet.Elem · cited by 7166Set.ElemunitInterval · cited by 607unitIntervalunitInterval.le_oneCITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Setstatement · cited by 53,352
  • Realstatement · cited by 25,697
  • Set.Elemstatement and proof · cited by 7,166
  • unitIntervalstatement and proof · cited by 607

Cited by3

Results whose statement or proof uses this declaration.