cRk_restrict — Mathlib

English

Alternative expression of the restricted rank relation: (M|X).cRk Y = M.cRk (X ∩ Y).

Русский

Альтернативное выражение отношения ранга в ограничении: (M|X).cRk Y = M.cRk(X ∩ Y).

LaTeX

$$$(M \\restriction X).\\mathrm{cRk} Y = M.\\mathrm{cRk}(X \\cap Y)$$$

Lean4

theorem cRk_restrict (M : Matroid α) (X Y : Set α) : (M ↾ X).cRk Y = M.cRk (X ∩ Y) := by
  rw [← cRk_inter_ground, restrict_ground_eq, cRk_restrict_subset _ inter_subset_right, inter_comm]

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