finite

Mathlib.Data.FunLike.Fintype

URI: https://scilib.ai/kg/mathlib#FunLike.finite

← MathLib Explorer

English

If α and γ are finite, then G is finite.

Русский

Если α и γ конечны, то G конечен.

LaTeX

$$$[Finite\ α] [Finite\ γ] \Rightarrow Finite G$$$

Lean4

/-- All `FunLike`s are finite if their domain and codomain are.

Non-dependent version of `DFunLike.finite` that might be easier to infer.
Can't be an instance because it can cause infinite loops.
-/
theorem finite [Finite α] [Finite γ] : Finite G :=
  DFunLike.finite G

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

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

Разделы

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

Аффилиация

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