surjOn_univ_of_subsingleton_nonempty

English

Under [Subsingleton β] and [Nonempty β], SurjOn f s univ is equivalent to s.Nonempty.

Русский

При [Subsingleton β] и [Nonempty β], SurjOn f s univ эквивалентно s.Nonempty.

LaTeX

$$$\\mathrm{SurjOn} f \\ s \\mathrm{univ} \\iff s \\neq \\varnothing$$$

Lean4

@[simp]
theorem surjOn_univ_of_subsingleton_nonempty [Subsingleton β] [Nonempty β] : SurjOn f s univ ↔ s.Nonempty := by
  cases nonempty_unique β; simp [univ_unique, Subsingleton.elim (f _) default, Set.Nonempty]

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