closure_disjoint_of_disjoint_of_subset_coloops

English

If X is disjoint from K and K ⊆ M.coloops, then the closure of X is disjoint from K: Disjoint(cl_M(X), K).

Русский

Если X не пересекается с K и K ⊆ M.coloops, то cl_M(X) не пересекается с K.

LaTeX

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

Lean4

theorem closure_disjoint_of_disjoint_of_subset_coloops (hXK : Disjoint X K) (hK : K ⊆ M.coloops) :
    Disjoint (M.closure X) K := by
  rwa [disjoint_iff_inter_eq_empty, closure_inter_eq_of_subset_coloops X hK, ← disjoint_iff_inter_eq_empty]

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