Mathlib Map

Theorems · Definition · order theory

OrderBot.lift

{α : Type u} →
  {β : Type v} →
    [inst : LE α] →
      [inst_1 : Bot α] →
        [inst_2 : LE β] → [inst_3 : OrderBot β] → (f : α → β) → (∀ (b a : α), f b ≤ f a → b ≤ a) → f ⊥ = ⊥ → OrderBot α

Pullback an OrderBot.

Defined in
Mathlib.Order.BoundedOrder.Basic
Cited by
0 results in Mathlib
Foundations
Depth 7 from the axioms · uses no axioms
Assumes
LEBotLEOrderBot
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

BoundedOrder.lift · cited by 0BoundedOrder.liftBot.bot · cited by 4720Bot.botOrderBot · cited by 1055OrderBotBot · cited by 96BotOrderBot.liftCITED BYCITES

Cites3

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
  • Botstatement and proof · cited by 96

Cited by1

Results whose statement or proof uses this declaration.