surjOn_of_subsingleton' — Mathlib

English

If β is a subsingleton, then for any f : α → β and any h: t.Nonempty → s.Nonempty, SurjOn f s t holds.

Русский

Если β — пододном, тогда для любого f: α→β и любого h: t.Nonempty → s.Nonempty, выполняется SurjOn f s t.

LaTeX

$$$ [\text{Subsingleton } \beta] \; (f: \alpha \to \beta) \; (h: t^{\text{Nonempty}} \to s^{\text{Nonempty}}) \;:\; \mathrm{SurjOn} f s t $$$

Lean4

theorem surjOn_of_subsingleton' [Subsingleton β] (f : α → β) (h : t.Nonempty → s.Nonempty) : SurjOn f s t := fun _ ha ↦
  Subsingleton.mem_iff_nonempty.2 <| (h ⟨_, ha⟩).image _

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