Mathlib Map

Theorems · Definition

OrderBot.copy

{α : Type u} → {h h' : LE α} → (c : OrderBot α) → (bot : α) → bot = ⊥ → (∀ (x y : α), x ≤ y ↔ x ≤ y) → OrderBot α

A function to create a provable equal copy of a bottom order with possibly different definitional equalities.

Defined in
Mathlib.Order.Copy
Cited by
1 results in Mathlib
Foundations
Depth 7 from the axioms · uses propext
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

GeneralizedCoheytingAlgebra.copy · cited by 1GeneralizedCoheytingAlgeb…HeytingAlgebra.copy · cited by 0HeytingAlgebra.copyOrderBot.copy.congr_simp · cited by 0copy.congr_simpBot.bot · cited by 4720Bot.botOrderBot · cited by 1055OrderBotBot · cited by 96BotOrderBot.copyCITED 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 · cited by 96

Cited by3

Results whose statement or proof uses this declaration.