removeNone_aux_none — Mathlib

English

For any x and e: Option α ≃ Option β, if e(some x) = none, then some (removeNone_aux e x) = e none.

Русский

Для любого x и e: Option α ≃ Option β, если e(Some x) = None, тогда Some (removeNone_aux e x) = e None.

LaTeX

$$$\\forall x\\: e(\\text{Some } x)=\\text{None} \\Rightarrow \\text{Some}(\\text{removeNone_aux } e\, x)= e(\\text{None}).$$$

Lean4

theorem removeNone_aux_none {x : α} (h : e (some x) = none) : some (removeNone_aux e x) = e none := by
  simp [removeNone_aux, Option.not_isSome_iff_eq_none.mpr h]

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