closure_insert_congr_right — Mathlib

English

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

Русский

Если для всех 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_insert_congr_right (h : M.closure X = M.closure Y) : M.closure (insert e X) = M.closure (insert e Y) :=
  by simp [← union_singleton, closure_union_congr_left h]

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