small_prod

Mathlib.Logic.Small.Basic

URI: https://scilib.ai/kg/mathlib#small_prod

← MathLib Explorer

English

If α and β are small, then α × β is small.

Русский

Если α и β малые, то α × β малое.

LaTeX

$$$ \\text{Small}(\\alpha \\times \\beta) $$$

Lean4

instance small_prod {α β} [Small.{w} α] [Small.{w} β] : Small.{w} (α × β) :=
  ⟨⟨Shrink α × Shrink β, ⟨Equiv.prodCongr (equivShrink α) (equivShrink β)⟩⟩⟩

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

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

Разделы

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

Аффилиация

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