English
If e : α ≃ β, then withTopCongr(e) gives an equivalence ᾰ → β̆ between WithTop α and WithTop β, with toFun = WithTop.map e and invFun = WithTop.map e.symm.
Русский
Если e: α ≃ β, то withTopCongr(e) даёт эквивалентность WithTop(α) и WithTop(β) с отображениями toFun = WithTop.map e и invFun = WithTop.map e.symm.
LaTeX
$$$\text{withTopCongr}(e) : WithTop(\alpha) \simeq WithTop(\beta)$$$
Lean4
/-- A universe-polymorphic version of `EquivFunctor.mapEquiv WithTop e`. -/
@[simps apply]
def withTopCongr (e : α ≃ β) : WithTop α ≃ WithTop β
where
toFun := WithTop.map e
invFun := WithTop.map e.symm
left_inv x := by cases x <;> simp
right_inv x := by cases x <;> simp
