English
If X and Y both have finite rank in M, then their union X ∪ Y also has finite rank in M.
Русский
Если X и Y имеют конечный ранг в M, то их объединение X ∪ Y также имеет конечный ранг в M.
LaTeX
$$$ M.IsRkFinite X \\rightarrow M.IsRkFinite Y \\rightarrow M.IsRkFinite(X \\cup Y) $$$
Lean4
theorem union (hX : M.IsRkFinite X) (hY : M.IsRkFinite Y) : M.IsRkFinite (X ∪ Y) :=
by
obtain ⟨I, hI, hIfin⟩ := hX.exists_finite_isBasis'
obtain ⟨J, hJ, hJfin⟩ := hY.exists_finite_isBasis'
rw [← isRkFinite_inter_ground_iff]
refine (M.isRkFinite_of_finite (hIfin.union hJfin)).closure.subset ?_
rw [closure_union_congr_left hI.closure_eq_closure, closure_union_congr_right hJ.closure_eq_closure]
exact inter_ground_subset_closure M (X ∪ Y)
