Mathlib Map

Theorems · Theorem · order theory

isBot_bot

∀ {α : Type u} [inst : LE α] [inst_1 : OrderBot α], IsBot ⊥
Defined in
Mathlib.Order.BoundedOrder.Basic
Cited by
9 results in Mathlib
Foundations
Depth 5 from the axioms · uses no axioms
Assumes
LEOrderBot
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

isMin_bot · cited by 15isMin_botSet.Ici_bot · cited by 10Set.Ici_botStieltjesFunction.measure_Iic · cited by 8StieltjesFunction.measure…Filter.OrderBot.atBot_eq · cited by 4OrderBot.atBot_eqisLeast_univ · cited by 3isLeast_univIsBot.rec · cited by 1IsBot.recSummationFilter.conditional_filter_eq_map_Iic · cited by 1SummationFilter.condition…StieltjesFunction.measure_Iio_of_tendsto_atBot_atBot · cited by 1StieltjesFunction.measure…isLUB_empty · cited by 1isLUB_emptySet.Iio_eq_singleton_iff · cited by 0Set.Iio_eq_singleton_iffBot.bot · cited by 4720Bot.botOrderBot · cited by 1055OrderBotbot_le · cited by 306bot_leIsBot · cited by 77IsBotisBot_botCITED BYCITES

Cites4

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

  • Bot.botstatement · cited by 4,720
  • OrderBotstatement and proof · cited by 1,055
  • bot_leproof · cited by 306
  • IsBotstatement · cited by 77

Cited by10

Results whose statement or proof uses this declaration.