Theorems · Theorem · order theory

Set.range_unique

∀ {α : Type u_1} {ι : Sort u_4} {f : ι → α} [inst : Unique ι], Set.range f = {f default}

The range of a function from a Unique type contains just the function applied to its single value.

Defined in

Mathlib.Data.Set.Image

Cited by

8 results in Mathlib

Foundations

Depth 10 from the axioms · uses propext, Quot.sound

Assumes

Unique