closure_inter_eq_of_subset_coloops

English

If K ⊆ coloops, then closure(X) ∩ K = X ∩ K for all X.

Русский

Если K ⊆ coloops, то closure(X) ∩ K = X ∩ K для всех X.

LaTeX

$$∀ X, Set.instHasSubset.Subset K M.coloops → Eq (Set.instInter.inter (M.closure X) K) (Set.instInter.inter X K)$$

Lean4

theorem closure_inter_eq_of_subset_coloops (X : Set α) (hK : K ⊆ M.coloops) : M.closure X ∩ K = X ∩ K :=
  by
  nth_rw 1 [← inter_eq_self_of_subset_right hK]
  rw [← inter_assoc, closure_inter_coloops_eq, inter_assoc, inter_eq_self_of_subset_right hK]

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