English
For an order isomorphism e: α ≃o β, there is a canonical order isomorphism between WithBot α and WithBot β extending e, obtained by applying e inside the WithBot construction.
Русский
Для упорядоченного изоморфизма e: α ≃o β существует каноническое упорядоченное изоморфизм между WithBot α и WithBot β, получаемый путем применения e внутри конструктора WithBot.
LaTeX
$$$ \mathrm{WithBotCongr}(e) : WithBot \alpha \cong_o WithBot \beta \text{ with } \mathrm{toFun} = \mathrm{WithBot.map}(e) $$$
Lean4
/-- A version of `Equiv.optionCongr` for `WithBot`. -/
@[simps -fullyApplied]
def withBotCongr (e : α ≃o β) : WithBot α ≃o WithBot β
where
toFun := WithBot.map e
__ := e.toOrderEmbedding.withBotMap
__ := e.toEquiv.withBotCongr
