closure_union_eq_of_subset_coloops

English

If K ⊆ coloops, then closure(X ∪ K) = closure(X) ∪ K.

Русский

Если K ⊆ coloops, то closure(X ∪ K) = closure(X) ∪ K.

LaTeX

$$$M.closure (X \\cup K) = M.closure X \\cup K$$$

Lean4

theorem closure_union_eq_of_subset_coloops (X : Set α) (hK : K ⊆ M.coloops) : M.closure (X ∪ K) = M.closure X ∪ K :=
  by
  rw [← closure_union_closure_left_eq, subset_antisymm_iff, and_iff_left (M.subset_closure _), ← diff_eq_empty,
    eq_empty_iff_forall_notMem]
  refine fun e ⟨hecl, he⟩ ↦ he (.inl ?_)
  obtain ⟨C, hCss, hC, heC⟩ := (mem_closure_iff_exists_isCircuit he).1 hecl
  rw [← singleton_union, ← union_assoc, union_comm, ← diff_subset_iff,
    (hC.disjoint_coloops.mono_right hK).sdiff_eq_left, singleton_union] at hCss
  exact M.closure_subset_closure_of_subset_closure (by simpa) <| hC.mem_closure_diff_singleton_of_mem heC

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