mk'

Mathlib.Logic.Small.Defs

URI: https://scilib.ai/kg/mathlib#Small.mk'

← MathLib Explorer

English

From an explicit equivalence e : α ≃ S, one obtains Small α.

Русский

Из явного эквивалентного отображения e : α ≃ S следует, что α мал.

LaTeX

$$$ \\text{Small}(\\alpha) \\;\\text{from } e: \\alpha \\simeq S $$$

Lean4

/-- Constructor for `Small α` from an explicit witness type and equivalence.
-/
theorem mk' {α : Type v} {S : Type w} (e : α ≃ S) : Small.{w} α :=
  ⟨⟨S, ⟨e⟩⟩⟩

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

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

Разделы

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

Аффилиация

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