closure_insert_eq_of_mem_closure — Mathlib

English

If for all i ∈ A, cl(Xi) = cl(Yi), then cl(⋃ i ∈ A Xi) = cl(⋃ i ∈ A Yi).

Русский

Если для всех i ∈ Acl(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_insert_eq_of_mem_closure (he : e ∈ M.closure X) : M.closure (insert e X) = M.closure X := by
  rw [← closure_insert_closure_eq_closure_insert, insert_eq_of_mem he, closure_closure]

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