removeNone_aux_some — Mathlib

English

For any x and an equivalence e: Option α ≃ Option β, if there exists x' with e(some x) = some x', then some (removeNone_aux e x) = e (some x).

Русский

Для любого x и эвалюации e: Option α ≃ Option β, если существует x' такое, что e(Some x) = Some x', тогда Some (removeNone_aux e x) = e(Some x).

LaTeX

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

Lean4

theorem removeNone_aux_some {x : α} (h : ∃ x', e (some x) = some x') : some (removeNone_aux e x) = e (some x) := by
  simp [removeNone_aux, Option.isSome_iff_exists.mpr h]

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