closure_disjoint_coloops_of_disjoint_coloops

English

If X is disjoint from M.coloops, then closure(X) is disjoint from M.coloops: Disjoint(cl_M(X), M.coloops).

Русский

Если X не пересекается с колоопами M, то замыкание X не пересекается с колоопами M.

LaTeX

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

Lean4

theorem closure_disjoint_coloops_of_disjoint_coloops (hX : Disjoint X (M.coloops)) : Disjoint (M.closure X) M.coloops :=
  closure_disjoint_of_disjoint_of_subset_coloops hX Subset.rfl

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