isRkFinite_iff_exists_isBasis' — Mathlib

English

A set X satisfies IsRkFinite M X iff there exists I with M.IsBasis' I X and I.Finite.

Русский

Множество X удовлетворяет IsRkFinite M X тогда и только тогда, когда существует I с M.IsBasis' I X и I.Finite.

LaTeX

$$$ M.IsRkFinite X \\iff \\exists I, M.IsBasis' I X \\land I.Finite $$$

Lean4

/-- A set satisfies `IsRkFinite` iff it has a finite basis' -/
theorem isRkFinite_iff_exists_isBasis' : M.IsRkFinite X ↔ ∃ I, M.IsBasis' I X ∧ I.Finite :=
  ⟨IsRkFinite.exists_finite_isBasis', fun ⟨_, hIX, hI⟩ ↦ hIX.isRkFinite_of_finite hI⟩

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