functional-programming - 将函数定义为 codomain 的子集

Question

我正在尝试将函数
f : A → B 的图像限制定义为 f': A → f[A]，其中 f'(a) = f(a) 。但是，我不确定如何在精益中定义它。
在我看来，最直观的定义方式是：

def fun_to_image {A B: Type*} (f: A → B): A → image f set.univ :=
        λ a, f a

但是，这会被拒绝，因为 (fa) 不是 B 类型（图像 f set.univ）。

我什至尝试证明 f(a) ∈ (image f univ) 。它没有帮助：

def fun_to_image (f : A → B) : A → image f univ := 
    λ a , 
    have h : f a ∈ image f univ := 
        exists.intro a 
            (and.intro trivial (eq.refl (f a))),
    f a

错误信息是：

type mismatch, term
  λ (a : A), f a
has type
  A → B
but is expected to have type
  A → ↥(f '' univ)

set.univ 和 image 在 data.set 中定义如下

def univ : set α :=
λ a, true

def image (f : α → β) (s : set α) : set β :=
{b | ∃ a, a ∈ s ∧ f a = b}

知道如何做到这一点吗？

Answer 1