closure_iUnion_closure_eq_closure_iUnion

English

For a family Xs indexed by ι, the closure of the union over i of the closures of Xs(i) equals the closure of the union of Xs(i).

Русский

Для семейства X_s индексируемого по ι выполнено: cl(⋃_i cl(X_i)) = cl(⋃_i X_i).

LaTeX

$$$\\operatorname{cl}\\Big(\\bigcup_i \\operatorname{cl}(X_i)\\Big) = \\operatorname{cl}\\Big(\\bigcup_i X_i\\Big)$$$

Lean4

theorem closure_iUnion_closure_eq_closure_iUnion (M : Matroid α) (Xs : ι → Set α) :
    M.closure (⋃ i, M.closure (Xs i)) = M.closure (⋃ i, Xs i) :=
  by
  simp_rw [closure_eq_subtypeClosure, iUnion_inter, Subtype.coe_inj]
  convert M.subtypeClosure.closure_iSup_closure (fun i ↦ ⟨Xs i ∩ M.E, inter_subset_right⟩) <;>
    simp [← iUnion_inter, subtypeClosure]

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