Mathlib Map

Theorems · Definition · order theory

AddEquiv.withTopCongr

{α : Type u} → {β : Type v} → [inst : Add α] → [inst_1 : Add β] → α ≃+ β → WithTop α ≃+ WithTop β

A AddEquiv version of Equiv.withTopCongr.

Defined in
Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Cited by
7 results in Mathlib
Foundations
Depth 17 from the axioms · uses propext, Quot.sound
Assumes
AddAdd
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

AddEquiv.withTopCongr_apply · cited by 1AddEquiv.withTopCongr_app…AddEquiv.withTopCongr_refl · cited by 0AddEquiv.withTopCongr_reflAddEquiv.withTopCongr_symm · cited by 0AddEquiv.withTopCongr_symmAddEquiv.withTopCongr_toAddHom · cited by 0AddEquiv.withTopCongr_toA…AddEquiv.withTopCongr_toEquiv · cited by 0AddEquiv.withTopCongr_toE…AddEquiv.withTopCongr_trans · cited by 0AddEquiv.withTopCongr_tra…AddEquiv.coe_withTopCongr · cited by 0AddEquiv.coe_withTopCongrEquiv · cited by 8337EquivWithTop · cited by 3754WithTopAddEquiv · cited by 1087AddEquivAddEquiv.toEquiv · cited by 174AddEquiv.toEquivEquiv.withTopCongr · cited by 5Equiv.withTopCongrAddEquiv.withTopCongrCITED BYCITES

Cites5

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

Cited by7

Results whose statement or proof uses this declaration.