range_eq — Mathlib

English

For any f: WithBot α → β, the range of f equals the set obtained by inserting f(⊥) into the range of f ∘ WithBot.some.

Русский

Для любого f: WithBot α → β множество образов f эквивалентно дополнению к множеству образов f ∘ WithBot.some элементом f(⊥).

LaTeX

$$$\operatorname{range} f = \operatorname{insert} (f\,\bot) (\operatorname{range} (f \circ WithBot.some))$$$

Lean4

theorem range_eq (f : WithBot α → β) : range f = insert (f ⊥) (range (f ∘ WithBot.some : α → β)) :=
  Option.range_eq f

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