removeNone_some — Mathlib

English

Let x ∈ α and suppose there exists x' with e(some x) = some x'. Then some (removeNone e x) = e (some x).

Русский

Пусть x ∈ α и существует x' такой, что e(некоторый x) = some x'. Тогда some(removeNone e x) = e(some x).

LaTeX

$$$\\forall x:\\alpha\\;\\big(\\exists x' : \\beta, e(\\mathrm{some}\\, x) = \\mathrm{some}\\, x'\\big)\\;\\Rightarrow\\; \\mathrm{some}(\\mathrm{removeNone}\, e\, x) = e(\\mathrm{some}\\, x).$$$

Lean4

theorem removeNone_some {x : α} (h : ∃ x', e (some x) = some x') : some (removeNone e x) = e (some x) :=
  removeNone_aux_some e h

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