encard_isBase_eq — Mathlib

English

All bases in a family with the exchange property have the same encard.

Русский

Все базы в семье со свойством обмена имеют одинаковый encard.

LaTeX

$$$$ B_1.encard = B_2.encard $$$$

Lean4

/-- Any two sets `B₁`, `B₂` in a family with the exchange property have the same
`ℕ∞`-cardinality. -/
theorem encard_isBase_eq (exch : ExchangeProperty IsBase) (hB₁ : IsBase B₁) (hB₂ : IsBase B₂) : B₁.encard = B₂.encard :=
  by rw [← encard_diff_add_encard_inter B₁ B₂, exch.encard_diff_eq hB₁ hB₂, inter_comm, encard_diff_add_encard_inter]

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