instFinitaryElemRestrictSubtype

Mathlib.Combinatorics.Matroid.Map

URI: https://scilib.ai/kg/mathlib#Matroid.instFinitaryElemRestrictSubtype

English

If M is finitary, then the restriction M.restrictSubtype X is also finitary.

Русский

Если M является конечным по определению, то ограничение M.restrictSubtype X также конечное.

LaTeX

$$$ [M\\text{ is Finite}] \\Rightarrow [ (M\\restrictSubtype X) \\text{ is Finite} ] $$$

Lean4

instance [M.Finitary] {X : Set α} : (M.restrictSubtype X).Finitary := by rw [restrictSubtype]; infer_instance

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

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

Разделы

Аффилиация

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