encard_diff_eq — Mathlib

English

The encard of B1 \ B2 equals the encard of B2 \ B1 when exchange holds.

Русский

encard(B1 \ B2) = encard(B2 \ B1).

LaTeX

$$$$ (B_1 \ B_2).encard = (B_2 \ B_1).encard $$$$

Lean4

/-- For any two sets `B₁`, `B₂` in a family with the exchange property, the differences `B₁ \ B₂`
and `B₂ \ B₁` have the same `ℕ∞`-cardinality. -/
theorem encard_diff_eq (exch : ExchangeProperty IsBase) (hB₁ : IsBase B₁) (hB₂ : IsBase B₂) :
    (B₁ \ B₂).encard = (B₂ \ B₁).encard :=
  (encard_diff_le_aux exch hB₁ hB₂).antisymm (encard_diff_le_aux exch hB₂ hB₁)

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