English
Let α and β be finite types and f: α → β an injective map. The inverse on the image, invOfMemRange : Set.range f → α, is surjective; equivalently, for every a ∈ α there exists b ∈ Set.range f with invOfMemRange(b) = a. In fact, for each a the witness can be taken as b = ⟨f a, mem_range_self a⟩.
Русский
Пусть α и β — конечные множества, $f: α \to β$ — инъекция. Обратное отображение на образе invOfMemRange : Set.range f → α сюръективно; то есть для каждого a ∈ α существует b ∈ Set.range f такое, что invOfMemRange(b) = a. Фактически для каждого a witness можно взять как b = ⟨f a, доказательство, что f a ∈ range f⟩.
LaTeX
$$$\\forall a : α, \\exists b \\in \\operatorname{range}(f), \\operatorname{invOfMemRange}(b) = a$$$
Lean4
theorem invOfMemRange_surjective : Function.Surjective hf.invOfMemRange := fun a =>
⟨⟨f a, Set.mem_range_self a⟩, by simp⟩
