Reference · Sets

rainbow.math.sets.range

Setssrc/rainbow/math/sets/range.clj1 definitions, 1 theorems

Lean-compatible Set range ordering and native finite-range laws.

set/lean-range.{u, v} :
  (B : Type v) (A : Type u) (mapping : A → B)
  → set/Set B

set/finite-range-constant.{u, v} :
  (A : Type u) (B : Type v) (selected : B)
  → set/finite B (set/lean-range B A (fun x₄ => selected))