prod_right

Mathlib.Data.Finite.Prod

URI: https://scilib.ai/kg/mathlib#Set.Infinite.prod_right

English

If t is infinite and s is nonempty, then s × t is infinite.

Русский

Если T бесконечно, а S непусто, то S × T бесконечно.

LaTeX

$$$ |t| = \infty \land s \neq \emptyset \Rightarrow |s| \times |t| = \infty $$$

Lean4

protected theorem prod_right (ht : t.Infinite) (hs : s.Nonempty) : (s ×ˢ t).Infinite := fun h =>
  ht <| h.of_prod_right hs

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

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

Разделы

Аффилиация

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