image₂

Mathlib.Data.Finset.NAry

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

← MathLib Explorer

English

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

Русский

Если s и t непусты, то image₂ f s t непуст.

LaTeX

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

Lean4

@[aesop safe apply (rule_sets := [finsetNonempty])]
theorem image₂ (hs : s.Nonempty) (ht : t.Nonempty) : (image₂ f s t).Nonempty :=
  image₂_nonempty_iff.2 ⟨hs, ht⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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