cardinalMk_diff_comm — Mathlib

English

If I and J are two bases of M contained in X, then the number of elements in I not in J equals the number of elements in J not in I: |I \ J| = |J \ I|.

Русский

Пусть I и J — базы матроида M над X. Тогда число элементов в I, не входящих в J, равно числу элементов в J, не входящих в I: |I \ J| = |J \ I|.

LaTeX

$$$|I \setminus J| = |J \setminus I|$$$

Lean4

theorem cardinalMk_diff_comm (hIX : M.IsBasis' I X) (hJX : M.IsBasis' J X) : #(I \ J : Set α) = #(J \ I : Set α) :=
  hIX.isBasis_inter_ground.cardinalMk_diff_comm hJX.isBasis_inter_ground

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