isRkFinite_diff_iff — Mathlib

English

If X has finite rank, then Y \\ X has finite rank if and only if Y has finite rank.\n(assuming X has finite rank as a hypothesis.)

Русский

Если X имеет конечный ранг, то Y \\ X имеет конечный ранг тогда и только тогда, когда Y имеет конечный ранг.

LaTeX

$$$ M.IsRkFinite X \\Rightarrow ( M.IsRkFinite (Y \\ X) \\leftrightarrow M.IsRkFinite Y ) $$$

Lean4

theorem isRkFinite_diff_iff (hX : M.IsRkFinite X) : M.IsRkFinite (Y \ X) ↔ M.IsRkFinite Y := by
  rw [← hX.isRkFinite_union_iff, union_diff_self, hX.isRkFinite_union_iff]

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