Mathlib Map

Theorems · Definition · order theory

OrderTop.lift

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

Pullback an OrderTop.

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

Around this declaration

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

BoundedOrder.lift · cited by 0BoundedOrder.liftTop.top · cited by 9680Top.topOrderTop · cited by 493OrderTopTop · cited by 93TopOrderTop.liftCITED BYCITES

Cites3

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

  • Top.topstatement and proof · cited by 9,680
  • OrderTopstatement and proof · cited by 493
  • Topstatement and proof · cited by 93

Cited by1

Results whose statement or proof uses this declaration.