Structures · Order
Bot
Typeclass for the ⊥ (\bot) notation
- Defined in
- Mathlib.Order.Notation
- Shape
- One type argument · adds bot
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by3
Forgetful instances
Every Bot is also a
Concrete types that are instances71
- NNReal
- ENNReal
- Filter.Germ
- ENat
- EReal
- UpperSet
- LowerSet
- LieSubalgebra
- LieSubmodule
- Associates
- TopologicalSpace.Compacts
- AddSubgroup
- AddSubmonoid
- Sublattice
- BooleanSubalgebra
- UniformSpace
- ValuativeRel.ValueGroupWithZero
- SimpleGraph.Subgraph
- MeasureTheory.OuterMeasure
- SubMulAction
- ConvexCone
- Finpartition
- LinearPMap
- TopologicalSpace.Clopens
- TwoSidedIdeal
- HomogeneousIdeal
- NonUnitalSubring
- NonUnitalSubsemiring
- SubAddAction
- AddSubsemigroup
- TopologicalSpace.CompactOpens
- CategoryTheory.Subgroupoid
- DividedPowers.SubDPIdeal
- AbstractSimplicialComplex
- PreAbstractSimplicialComplex
- MeasureTheory.Filtration
- FirstOrder.Language.DefinableSet
- CategoryTheory.Precoverage
- Ideal.Filtration
- GroupTopology
- AddGroupTopology
- Heyting.Regular
- Booleanisation
- ClopenUpperSet
- InfHom
- SupHom
- PEquiv
- Geometry.SimplicialComplex
- sSupHom
- PseudoMetric
- FirstOrder.Language.BoundedFormula
- CategoryTheory.MonoOver
- WideSubquiver
- Hypergraph
- Subtype
- Prod
- OrderDual
- Set.Elem
- ULift
- Shrink
- WithTop
- WithBot
- Submodule
- WithZero
- Filter
- Subgroup
- OrderHom
- Submonoid
- Subring
- Subsemiring
- Subsemigroup
How is a type an instance?
Loading the hierarchy index…
Assumed by143
- Bot.bot
- SupBotHom.comp
- BotHom.comp
- SupBotHom.id
- BotHom.id
- SupBotHom.dual
- WithTop.sub_top
- SupBotHom.toSupHom
- Pi.bot_comp
- WithTop.sub_eq_top_iff
- Pi.bot_apply
- BotHom.copy
- SupBotHom.copy
- WithTop.sub_ne_top_iff
- WithTop.coe_bot
- Equiv.bot
- BotHom.toFun
- SupBotHom.toBotHom
- WithTop.coe_sub
- SupBotHom.comp_apply
- BotHom.comp_apply
- WithTop.coe_eq_bot
- dite_ne_bot
- SupBotHom.coe_mk
- BotHomClass.toBotHom
- WithTop.map_sub
- SupBotHom.id_toFun
- SupBotHom.dual_comp
- OrderBot.lift
- OrderDual.instTopOfBot
- SupBotHom.symm_dual_id
- BotHom.instMin
- SupHom.coe_bot
- BotHom.instLE
- instCoeTCBotHomOfBotHomClass
- SupBotHom.instOrderBot
- OrderDual.toDual_bot
- ULift.instBot
- Function.Injective.completeBooleanAlgebra
- SupBotHom.coe_toBotHom
- BotHom.instFunLike
- equivShrink_symm_bot
- Prod.instBot
- BotHom.sup_apply
- SupBotHom.sup_apply
- equivShrink_bot
- SupBotHom.dual_id
- BotHom.instLattice
- SupBotHom.coe_sup
- Function.Injective.heytingAlgebra