ncard_diff_comm — Mathlib

English

If B1 and B2 are bases of M, then the ncard (finite cardinality) of B1 \ B2 equals that of B2 \ B1.

Русский

Если B1 и B2 — базы M, то ncard(B1 \ B2) = ncard(B2 \ B1).

LaTeX

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

Lean4

theorem ncard_diff_comm (hB₁ : M.IsBase B₁) (hB₂ : M.IsBase B₂) : (B₁ \ B₂).ncard = (B₂ \ B₁).ncard := by
  rw [ncard_def, hB₁.encard_diff_comm hB₂, ← ncard_def]

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