English
For any equivalence e: α ≃ β, there is an induced equivalence between WithBot α and WithBot β given by map on the right and its inverse by map e.symm.
Русский
Для любого эквивалентности e: α ≃ β существует индуцированная эквивалентность между WithBot α и WithBot β, заданная отображением map на слое и обратным отображением map e.symm.
LaTeX
$$$\forall e : α ≃ β,\; WithBot.map e : WithBot α ≃ WithBot β$$$
Lean4
/-- A universe-polymorphic version of `EquivFunctor.mapEquiv WithBot e`. -/
@[simps apply]
def withBotCongr (e : α ≃ β) : WithBot α ≃ WithBot β
where
toFun := WithBot.map e
invFun := WithBot.map e.symm
left_inv x := by cases x <;> simp
right_inv x := by cases x <;> simp
