diff_finite_comm — Mathlib

English

For bases B1, B2, the infiniteness of B1 \ B2 is equivalent to the infiniteness of B2 \ B1.

Русский

Для баз B1, B2 бесконечность B1 \ B2 эквивалентна бесконечности B2 \ B1.

LaTeX

$$(hB1 : M.IsBase B1) → (hB2 : M.IsBase B2) → (B1 \ B2).Infinite ↔ (B2 \ B1).Infinite$$

Lean4

theorem diff_finite_comm (hB₁ : M.IsBase B₁) (hB₂ : M.IsBase B₂) : (B₁ \ B₂).Finite ↔ (B₂ \ B₁).Finite :=
  finite_iff_finite_of_encard_eq_encard (hB₁.encard_diff_comm hB₂)

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