removeNone_none — Mathlib

English

If e maps some x to none, then some (removeNone e x) equals none under e, i.e., some (removeNone e x) = e none.

Русский

Если e отображает some x в none, то some (removeNone e x) равняется e none.

LaTeX

$$$\forall x:\alpha,\; e(\mathrm{some}\, x) = \mathrm{none} \Rightarrow \mathrm{some}(\mathrm{removeNone}\, e\, x) = e(\mathrm{none}).$$$

Lean4

theorem removeNone_none {x : α} (h : e (some x) = none) : some (removeNone e x) = e none :=
  removeNone_aux_none e h

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