surjOn_singleton

Mathlib.Data.Set.Function

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

English

SurjOn f s {b} holds iff b ∈ f''s.

Русский

SurjOn f s {b} эквивалентно тому, что b принадлежит образу f(S).

LaTeX

$$$\\mathrm{SurjOn} f \\ s \\ {b} \\iff b \\in f''s$$

Lean4

@[simp]
theorem surjOn_singleton : SurjOn f s { b } ↔ b ∈ f '' s :=
  singleton_subset_iff

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

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

Разделы

Аффилиация

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