range_unique — Mathlib

English

If the domain is a Unique type, then the range of any function f: ι → α is the singleton { f default }.

Русский

Если область определения является уникальным типом, то образ функции f: ι → α равен одиночному множеству { f(default) }.

LaTeX

$$$$ \\operatorname{range}(f) = \\{ f(\\mathrm{default}) \\} $$$$

Lean4

/-- The range of a function from a `Unique` type contains just the
function applied to its single value. -/
theorem range_unique [h : Unique ι] : range f = {f default} :=
  by
  ext x
  rw [mem_range]
  constructor
  · rintro ⟨i, hi⟩
    rw [h.uniq i] at hi
    grind
  · grind

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