invOfMemRange_surjective — Mathlib

English

As above, the inverse on the image invOfMemRange is surjective: for every a ∈ α there exists b ∈ Set.range f with invOfMemRange(b) = a.

Русский

Как выше, invOfMemRange на образе сюръективно: для каждого a ∈ α существует b ∈ Set.range f такое, что invOfMemRange(b) = a.

LaTeX

$$$\\forall a : α, \\exists b \\in \\operatorname{range}(f), \\operatorname{invOfMemRange}(b)=a$$$

Lean4

theorem invOfMemRange_surjective : Function.Surjective f.invOfMemRange := fun a =>
  ⟨⟨f a, Set.mem_range_self a⟩, by simp⟩

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