insert_none_range_some — Mathlib

English

Let α be any type. The range of the Some map, together with None, covers all elements of the option type: every element of Option α is either None or Some(a) for some a ∈ α.

Русский

Пусть α — произвольный тип. Область значения отображения Some(·) вместе с None покрывает все элементы типа Option α: любой элемент Option α либо равен None, либо равен Some(a) для некоторого a ∈ α.

LaTeX

$$$\operatorname{Option}(\alpha) = \{ \mathrm{None} \} \cup \{ \mathrm{Some}(a) \mid a \in \alpha \}.$$$

Lean4

@[simp]
theorem insert_none_range_some (α : Type*) : insert none (range (some : α → Option α)) = univ :=
  (isCompl_range_some_none α).symm.sup_eq_top

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