diff_singleton_iff — Mathlib

English

Removing a single element preserves finite rank: M.IsRkFinite (X \\ {e}) iff M.IsRkFinite X.

Русский

Удаление одного элемента сохраняет конечный ранг: M.IsRkFinite(X \\ {e}) эквивалентно M.IsRkFinite X.

LaTeX

$$$ M.IsRkFinite (X \\ {e}) \\leftrightarrow M.IsRkFinite X $$$

Lean4

@[simp]
theorem diff_singleton_iff : M.IsRkFinite (X \ { e }) ↔ M.IsRkFinite X := by
  rw [isRkFinite_singleton.isRkFinite_diff_iff]

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