closure_diff_eq_of_subset_coloops

English

For any X and K with K ⊆ M.coloops, the closure distributes over set difference: cl_M(X \ K) = cl_M(X) \ K.

Русский

Для любых X и K, удовлетворяющих K ⊆ M.coloops, замыкание распределяется по разности: cl_M(X \ K) = cl_M(X) \ K.

LaTeX

$$$$ M.closure(X \setminus K) = M.closure(X) \setminus K \quad \text{при } K \subseteq M.coloops. $$$$

Lean4

theorem closure_diff_eq_of_subset_coloops (X : Set α) (hK : K ⊆ M.coloops) : M.closure (X \ K) = M.closure X \ K :=
  by
  nth_rw 2 [← inter_union_diff X K]
  rw [union_comm, closure_union_eq_of_subset_coloops _ (inter_subset_right.trans hK), union_diff_distrib,
    diff_eq_empty.mpr inter_subset_right, union_empty, eq_comm, sdiff_eq_self_iff_disjoint, disjoint_iff_forall_ne]
  rintro e heK _ heX rfl
  rw [IsColoop.mem_closure_iff_mem (hK heK)] at heX
  exact heX.2 heK

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