of_image₂_right

Mathlib.Data.Finset.NAry

URI: https://scilib.ai/kg/mathlib#Finset.Nonempty.of_image₂_right

English

If image₂ f s t is nonempty, then t is nonempty.

Русский

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

LaTeX

$$$(\\operatorname{image}_2 f s t).Nonempty \\Rightarrow t.Nonempty$$$

Lean4

theorem of_image₂_right (h : (s.image₂ f t).Nonempty) : t.Nonempty :=
  (image₂_nonempty_iff.1 h).2

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

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

Разделы

Аффилиация

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