of_vsub_right

Mathlib.Algebra.Group.Pointwise.Finset.Scalar

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

English

If (s -ᵥ t).Nonempty, then t.Nonempty.

Русский

Если (s -ᵥ t) непусто, то t непусто.

LaTeX

$$$ (s -ᵥ t).Nonempty \Rightarrow t.Nonempty $$$

Lean4

theorem of_vsub_right : (s -ᵥ t : Finset α).Nonempty → t.Nonempty :=
  Nonempty.of_image₂_right

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

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

Разделы

Аффилиация

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