range_eq — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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