English
If Xs and Ys are families indexed by ι with cl(Xs i) = cl(Ys i) for all i in A, then the closures of their biunions are equal.
Русский
Если Xs и Ys—семейства, индексируемые ι, и для всех i ∈ A выполнено cl(Xi) = cl(Yi), то cl(⋃ i ∈ A Xi) = cl(⋃ i ∈ A Yi).
LaTeX
$$$\\forall i \\in A, \\operatorname{cl}(X_i) = \\operatorname{cl}(Y_i) \\Rightarrow \\operatorname{cl}(\\bigcup_{i \\in A} X_i) = \\operatorname{cl}(\\bigcup_{i \\in A} Y_i)$$$
Lean4
theorem closure_biUnion_congr (M : Matroid α) (Xs Ys : ι → Set α) (A : Set ι)
(h : ∀ i ∈ A, M.closure (Xs i) = M.closure (Ys i)) : M.closure (⋃ i ∈ A, Xs i) = M.closure (⋃ i ∈ A, Ys i) := by
rw [← closure_biUnion_closure_eq_closure_biUnion, iUnion₂_congr h, closure_biUnion_closure_eq_closure_biUnion]
