finite_of_subset_isRkFinite

Mathlib.Combinatorics.Matroid.Rank.Finite

URI: https://scilib.ai/kg/mathlib#Matroid.Indep.finite_of_subset_isRkFinite

English

If I is independent and I ⊆ X, and X has finite rank, then I is finite.

Русский

Если I независимо и I ⊆ X, и X имеет конечный ранг, тогда I конечно.

LaTeX

$$M.Indep I \\wedge I \\subseteq X \\wedge M.IsRkFinite X \\Rightarrow I.Finite$$

Lean4

theorem finite_of_subset_isRkFinite (hI : M.Indep I) (hIX : I ⊆ X) (hX : M.IsRkFinite X) : I.Finite :=
  hX.finite_of_indep_subset hI hIX

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

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

Разделы

Аффилиация

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