inter_right

Mathlib.Combinatorics.Matroid.Rank.Finite

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

English

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

Русский

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

LaTeX

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

Lean4

theorem inter_right (hX : M.IsRkFinite X) : M.IsRkFinite (X ∩ Y) :=
  hX.subset inter_subset_left

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

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

Разделы

Аффилиация

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