isRkFinite_union_iff — Mathlib

English

If X has finite rank, then M.IsRkFinite(X ∪ Y) is equivalent to M.IsRkFinite(Y).

Русский

Если X имеет конечный ранг, то M.IsRkFinite(X ∪ Y) эквивалентно M.IsRkFinite(Y).

LaTeX

$$$ M.IsRkFinite X \\rightarrow ( M.IsRkFinite(X \\cup Y) \\leftrightarrow M.IsRkFinite Y ) $$$

Lean4

theorem isRkFinite_union_iff (hX : M.IsRkFinite X) : M.IsRkFinite (X ∪ Y) ↔ M.IsRkFinite Y :=
  ⟨fun h ↦ h.subset subset_union_right, fun h ↦ hX.union h⟩

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