small

Mathlib.ModelTheory.Encoding

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.Term.small

English

If α is small, then L.Term α is small as well.

Русский

Если α небольшого кардинала, то и L.Term α небольшого кардинала.

LaTeX

$$[Small α] ⇒ [Small (L.Term α)]$$

Lean4

instance small [Small.{u} α] : Small.{u} (L.Term α) :=
  small_of_injective listEncode_injective

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

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

Разделы

Аффилиация

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