inter_left

Mathlib.Combinatorics.Matroid.Rank.Finite

URI: https://scilib.ai/kg/mathlib#Matroid.IsRkFinite.inter_left

English

If X has finite rank in M, then Y ∩ X has finite rank in M.

Русский

Если X имеет конечный ранг в M, то Y ∩ X имеет конечный ранг.

LaTeX

$$$ M.IsRkFinite X \\rightarrow M.IsRkFinite (Y \\cap X) $$$

Lean4

theorem inter_left (hX : M.IsRkFinite X) : M.IsRkFinite (Y ∩ X) :=
  hX.subset inter_subset_right

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

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

Разделы

Аффилиация

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