mem_image_univ_iff_mem_range — Mathlib

English

For a finite domain α and any function f: α → β, the image of f on the whole domain equals the range of f.

Русский

Для конечного домена α и любой функции f: α → β образ всей области совпадает с областью значений функции f.

LaTeX

$$$b \in univ.image f \iff b \in \mathrm{range}(f)$$$

Lean4

theorem mem_image_univ_iff_mem_range {α β : Type*} [Fintype α] [DecidableEq β] {f : α → β} {b : β} :
    b ∈ univ.image f ↔ b ∈ Set.range f := by simp

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