instFinite

Mathlib.Data.SetLike.Fintype

URI: https://scilib.ai/kg/mathlib#SetLike.instFinite

English

If B is finite, then A is finite (the Finite instance for SetLike).

Русский

Если B конечен, то A конечен (инстанс Finite для SetLike).

LaTeX

$$$ \text{Finite}(B) \Rightarrow \text{Finite}(A) $$$

Lean4

instance (priority := 100) {A B : Type*} [SetLike A B] [Finite B] : Finite A :=
  Finite.of_injective SetLike.coe SetLike.coe_injective

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

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

Разделы

Аффилиация

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