closure_sdiff_eq_closure — Mathlib

English

If t is contained in the closure of s \\ t, then closure(s \\ t) = closure(s).

Русский

Если t ⊆ closure(s \\ t), то closure(s \\ t) = closure(s).

LaTeX

$$$\\text{hts}: t \\subseteq \\operatorname{closure}(s \\setminus t) \\quad\\Rightarrow\\quad \\operatorname{closure}(s \\setminus t) = \\operatorname{closure}(s)$$$

Lean4

@[to_additive] -- this must not be a simp-lemma as the conclusion applies to `hts`, causing loops

theorem closure_sdiff_eq_closure (hts : t ⊆ closure (s \ t)) : closure (s \ t) = closure s :=
  by
  refine (closure_mono Set.diff_subset).antisymm <| closure_le.mpr <| fun x hxs ↦ ?_
  by_cases hxt : x ∈ t
  · exact hts hxt
  · rw [SetLike.mem_coe, Submonoid.mem_closure]
    exact fun N hN ↦ hN <| Set.mem_diff_of_mem hxs hxt

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