of_equiv

Mathlib.Data.Finite.Defs

URI: https://scilib.ai/kg/mathlib#Finite.of_equiv

English

If α is finite and f: α ≃ β is an equivalence, then β is finite.

Русский

Если α конечна и f: α ≃ β — эквиваленция, то β конечно.

LaTeX

$$$\forall \alpha\beta, \ (f:\\alpha \\\simeq \\beta) \\Rightarrow \\operatorname{Finite}(\\alpha) \\Rightarrow \\operatorname{Finite}(\\beta).$$$

Lean4

theorem of_equiv (α : Sort*) [h : Finite α] (f : α ≃ β) : Finite β :=
  let ⟨e⟩ := h;
  ⟨f.symm.trans e⟩

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

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

Разделы

Аффилиация

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