Mathlib Map

Theorems · Definition · order theory

IsBot.rec

{α : Type u} →
  [inst : LE α] →
    {motive : (x : α) → IsBot x → Sort u_1} →
      ([inst_1 : OrderBot α] → motive ⊥ ⋯) → (x : α) → (hx : IsBot x) → motive x hx

A bottom element can be replaced with ⊥. Prefer IsBot.eq_bot if α already has a bottom element.

Defined in
Mathlib.Order.BoundedOrder.Basic
Cited by
1 results in Mathlib
Foundations
Depth 6 from the axioms · uses no axioms
Assumes
LE
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Set.Iio_eq_singleton_iff · cited by 0Set.Iio_eq_singleton_iffBot.bot · cited by 4720Bot.botOrderBot · cited by 1055OrderBotIsBot · cited by 77IsBotisBot_bot · cited by 9isBot_botIsBot.recCITED BYCITES

Cites4

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
  • OrderBotstatement and proof · cited by 1,055
  • IsBotstatement and proof · cited by 77
  • isBot_botstatement and proof · cited by 9

Cited by1

Results whose statement or proof uses this declaration.