Mathlib Map

Theorems · Theorem · order theory

Pi.bot_comp

∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : Bot γ] (x : α → β), ⊥ ∘ x = ⊥
Defined in
Mathlib.Order.BoundedOrder.Basic
Cited by
3 results in Mathlib
Foundations
Depth 3 from the axioms · uses no axioms
Assumes
Bot
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Monotone.linearGrowthSup_comp · cited by 2Monotone.linearGrowthSup_…Monotone.linearGrowthInf_comp · cited by 2Monotone.linearGrowthInf_…Monotone.linearGrowthInf_comp_le · cited by 2Monotone.linearGrowthInf_…Bot.bot · cited by 4720Bot.botBot · cited by 96BotPi.bot_compCITED BYCITES

Cites2

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

  • Bot.botstatement and proof · cited by 4,720
  • Botstatement and proof · cited by 96

Cited by3

Results whose statement or proof uses this declaration.