comap_nonempty

Mathlib.Data.Set.Function

URI: https://scilib.ai/kg/mathlib#Set.SurjOn.comap_nonempty

English

If h: SurjOn f s t and t is nonempty, then s is nonempty.

Русский

Если f отображает s на t и t непусто, то s непусто.

LaTeX

$$$$ \\operatorname{SurjOn}(f,s,t) \\land t \\neq \\varnothing \\Rightarrow s \\neq \\varnothing $$$$

Lean4

theorem comap_nonempty (h : SurjOn f s t) (ht : t.Nonempty) : s.Nonempty :=
  (ht.mono h).of_image

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

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

Разделы

Аффилиация

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