Mathlib Map

Theorems · Theorem · order theory

Pi.top_def

∀ {ι : Type u_1} {α' : ι → Type u_2} [inst : (i : ι) → Top (α' i)], ⊤ = fun x => ⊤
Defined in
Mathlib.Order.BoundedOrder.Basic
Cited by
2 results in Mathlib
Foundations
Depth 3 from the axioms · uses no axioms
Assumes
Top
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

LinearGrowth.linearGrowthInf_comp_nonneg · cited by 3LinearGrowth.linearGrowth…ExpGrowth.expGrowthInf_of_eventually_ge · cited by 0ExpGrowth.expGrowthInf_of…Top.top · cited by 9680Top.topTop · cited by 93TopPi.top_defCITED BYCITES

Cites2

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

  • Top.topstatement · cited by 9,680
  • Topstatement and proof · cited by 93

Cited by2

Results whose statement or proof uses this declaration.