image_univ_of_surjective — Mathlib

English

If f : β → α is surjective and α is finite, then the image of the universe under f is the universe: univ.image f = univ.

Русский

Пусть f : β → α сюръективно, и α конечен; образ вселенной под f равен вселенной.

LaTeX

$$$ univ.image f = univ $$$

Lean4

theorem image_univ_of_surjective [Fintype β] {f : β → α} (hf : Surjective f) : univ.image f = univ :=
  eq_univ_of_forall <| hf.forall.2 fun _ => mem_image_of_mem _ <| mem_univ _

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