range_eq — Mathlib

English

For any f: Option α → β, the range of f is the union of the image of none and the range of f on some elements.

Русский

Для любого отображения f: Option α → β множество значений функции равно объединению образа значения None и множества значений на Some.

LaTeX

$$$\operatorname{range}(f) = \operatorname{insert}(f(\mathrm{none})) (\operatorname{range}(f \circ \mathrm{Some}))$$$

Lean4

theorem range_eq {α β} (f : Option α → β) : range f = insert (f none) (range (f ∘ some)) :=
  Set.ext fun _ => Option.exists.trans <| eq_comm.or Iff.rfl

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