def AddEquiv.withBotCongr {α : Type u_1} {β : Type u_2} [Add α] [Add β] (e : α ≃+ β) : WithBot α ≃+ WithBot β

Equations

• e.withBotCongr = { toEquiv := e.withBotCongr, map_add' := ⋯ }

def AddEquiv.withTopCongr {α : Type u_1} {β : Type u_2} [Add α] [Add β] (e : α ≃+ β) : WithTop α ≃+ WithTop β

Equations

• e.withTopCongr = { toEquiv := e.withTopCongr, map_add' := ⋯ }

@[simp]

theorem AddEquiv.coe_withBotCongr {α : Type u_1} {β : Type u_2} [Add α] [Add β] (e : α ≃+ β) : ⇑e.withBotCongr = WithBot.map ⇑e

@[simp]

theorem AddEquiv.coe_withTopCongr {α : Type u_1} {β : Type u_2} [Add α] [Add β] (e : α ≃+ β) : ⇑e.withTopCongr = WithTop.map ⇑e

theorem AddEquiv.coe_withBotCongr_eq_equiv_withBotCongr {α : Type u_1} {β : Type u_2} [Add α] [Add β] (e : α ≃+ β) : ↑e.withBotCongr = (↑e).withBotCongr

theorem AddEquiv.coe_withTopCongr_eq_equiv_withTopCongr {α : Type u_1} {β : Type u_2} [Add α] [Add β] (e : α ≃+ β) : ↑e.withTopCongr = (↑e).withTopCongr

theorem AddEquiv.coe_withBotCongr_eq_addHom_withBotMap {α : Type u_1} {β : Type u_2} [Add α] [Add β] (e : α ≃+ β) : ↑e.withBotCongr = (↑e).withBotMap

theorem AddEquiv.coe_withTopCongr_eq_addHom_withTopMap {α : Type u_1} {β : Type u_2} [Add α] [Add β] (e : α ≃+ β) : ↑e.withTopCongr = (↑e).withBotMap

theorem AddEquiv.withBotCongr_apply {α : Type u_1} {β : Type u_2} [Add α] [Add β] (e : α ≃+ β) (a : WithBot α) : e.withBotCongr a = WithBot.map (⇑e) a

theorem AddEquiv.withTopCongr_apply {α : Type u_1} {β : Type u_2} [Add α] [Add β] (e : α ≃+ β) (a : WithTop α) : e.withTopCongr a = WithTop.map (⇑e) a

@[simp]

theorem AddEquiv.withBotCongr_refl {α : Type u_1} [Add α] : (refl α).withBotCongr = refl (WithBot α)

@[simp]

theorem AddEquiv.withTopCongr_refl {α : Type u_1} [Add α] : (refl α).withTopCongr = refl (WithTop α)

@[simp]

theorem AddEquiv.withBotCongr_symm {α : Type u_1} {β : Type u_2} [Add α] [Add β] (e : α ≃+ β) : e.symm.withBotCongr = e.withBotCongr.symm

@[simp]

theorem AddEquiv.withTopCongr_symm {α : Type u_1} {β : Type u_2} [Add α] [Add β] (e : α ≃+ β) : e.symm.withTopCongr = e.withTopCongr.symm

@[simp]

theorem AddEquiv.withBotCongr_trans {α : Type u_1} {β : Type u_3} {γ : Type u_2} [Add α] [Add β] [Add γ] (e₁ : α ≃+ β) (e₂ : β ≃+ γ) : (e₁.trans e₂).withBotCongr = e₁.withBotCongr.trans e₂.withBotCongr

@[simp]

theorem AddEquiv.withTopCongr_trans {α : Type u_1} {β : Type u_3} {γ : Type u_2} [Add α] [Add β] [Add γ] (e₁ : α ≃+ β) (e₂ : β ≃+ γ) : (e₁.trans e₂).withTopCongr = e₁.withTopCongr.trans e₂.withTopCongr