of_image2_left

Mathlib.Data.Set.NAry

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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