small_map

Mathlib.Logic.Small.Defs

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

English

If α ≃ β and β is small, then α is small.

Русский

Если α эквивалентно β и β мала, то α мала.

LaTeX

$$$(e:\alpha \simeq \beta) \Rightarrow (Small(\beta) \Rightarrow Small(\alpha)).$$$

Lean4

theorem small_map {α : Type*} {β : Type*} [hβ : Small.{w} β] (e : α ≃ β) : Small.{w} α :=
  let ⟨_, ⟨f⟩⟩ := hβ.equiv_small
  Small.mk' (e.trans f)

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

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

Разделы

Аффилиация

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