encard_diff_comm — Mathlib

English

If B1 and B2 are bases of M, then the encard (cardinality in ENat) of B1 \ B2 equals that of B2 \ B1.

Русский

Пусть B1 и B2 — базы M. Тогда encard множества B1 \ B2 равна encard множества B2 \ B1.

LaTeX

$$$(hB_1 : M.IsBase B_1) \to (hB_2 : M.IsBase B_2) \to (B_1 \ B_2).encard = (B_2 \ B_1).encard$$$

Lean4

theorem encard_diff_comm (hB₁ : M.IsBase B₁) (hB₂ : M.IsBase B₂) : (B₁ \ B₂).encard = (B₂ \ B₁).encard :=
  M.isBase_exchange.encard_diff_eq hB₁ hB₂

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