isRkFinite_insert_iff — Mathlib

English

The finite-rank property is invariant under adding a single element: M.IsRkFinite (insert e X) iff M.IsRkFinite X.

Русский

Свойство конечного ранга не изменяется при добавлении одного элемента: M.IsRkFinite(insert e X) эквивалентно M.IsRkFinite X.

LaTeX

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

Lean4

@[simp]
theorem isRkFinite_insert_iff {e : α} : M.IsRkFinite (insert e X) ↔ M.IsRkFinite X := by
  rw [← singleton_union, isRkFinite_singleton.isRkFinite_union_iff]

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