surjOn_empty

Mathlib.Data.Set.Function

URI: https://scilib.ai/kg/mathlib#Set.surjOn_empty

English

For any f and s, SurjOn f s ∅ holds.

Русский

Для любых f и s справедливо SurjOn f s ∅.

LaTeX

$$$\\forall f\\,\\forall s\\ SurjOn f\\ s\\ emptyset$.$$

Lean4

theorem surjOn_empty (f : α → β) (s : Set α) : SurjOn f s ∅ :=
  empty_subset _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru