removeNone_optionCongr — Mathlib

English

The map e ↦ e.optionCongr from α ≃ β to Option α ≃ Option β is injective.

Русский

Отображение e ↦ e.optionCongr из α ≃ β в Option α ≃ Option β инъективно.

LaTeX

$$$\forall e_1,e_2,\; \mathrm{optionCongr}(e_1)=\mathrm{optionCongr}(e_2) \Rightarrow e_1=e_2.$$$

Lean4

@[simp]
theorem removeNone_optionCongr (e : α ≃ β) : removeNone e.optionCongr = e :=
  Equiv.ext fun x => Option.some_injective _ <| removeNone_some _ ⟨e x, by simp⟩

Похожие утверждения