vsub

Mathlib.Algebra.Group.Pointwise.Finset.Scalar

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

English

If s and t are nonempty Finsets, then s -ᵥ t is nonempty.

Русский

Пусть s и t — непустые конечные множества, тогда s -ᵥ t непусто.

LaTeX

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

Lean4

@[aesop safe apply (rule_sets := [finsetNonempty])]
theorem vsub : s.Nonempty → t.Nonempty → (s -ᵥ t : Finset α).Nonempty :=
  Nonempty.image₂

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

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

Разделы

Аффилиация

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