small_sum

Mathlib.Logic.Small.Basic

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

instance small_sum {α β} [Small.{w} α] [Small.{w} β] : Small.{w} (α ⊕ β) :=
  ⟨⟨Shrink α ⊕ Shrink β, ⟨Equiv.sumCongr (equivShrink α) (equivShrink β)⟩⟩⟩

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

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

Разделы

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

Аффилиация

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