Mathlib Map

Theorems · Inductive type

Top

Type u_1 → Type u_1

Typeclass for the ⊤ (\top) notation

Defined in
Mathlib.Order.Notation
Cited by
93 results in Mathlib
Foundations
Depth 0 from the axioms, rests on 1 definitions · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Top.top · cited by 9680Top.topInfTopHom · cited by 60InfTopHomTopHom · cited by 37TopHomTopHomClass.map_top · cited by 14TopHomClass.map_topENNReal.mul_iSup · cited by 13ENNReal.mul_iSupInfTopHom.comp · cited by 12InfTopHom.compTopHom.comp · cited by 12TopHom.compAlgebra.FiniteType.of_surjective · cited by 11FiniteType.of_surjectiveInfTopHom.id · cited by 10InfTopHom.idInfTopHom.toInfHom · cited by 10InfTopHom.toInfHomTopHom.id · cited by 8TopHom.idENNReal.top_mul' · cited by 7ENNReal.top_mul'InfTopHom.dual · cited by 5InfTopHom.dualTopHom.ext · cited by 5TopHom.extWithBot.coe_top · cited by 4WithBot.coe_topTopCITED BYCITES

Cites0

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

Nothing in Mathlib beyond the foundations.

Cited by170

Results whose statement or proof uses this declaration.