of_image2_right

Mathlib.Data.Set.NAry

URI: https://scilib.ai/kg/mathlib#Set.Nonempty.of_image2_right

English

If image2 f S T is nonempty, then T is nonempty.

Русский

Если образ image2 f S T непуст, то T непусто.

LaTeX

$$$$ (\\operatorname{image2} f S T).Nonempty \\Rightarrow T.Nonempty. $$$$

Lean4

theorem of_image2_right (h : (Set.image2 f s t).Nonempty) : t.Nonempty :=
  (image2_nonempty_iff.1 h).2

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

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

Разделы

Аффилиация

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