mem_closure_of_mem_closure_union — Mathlib

English

If x lies in the closure of s1 ∪ s2 and the complement of s1 is a neighborhood of x, then x lies in the closure of s2.

Русский

Если точка x принадлежит замыканию множества s1 ∪ s2 и дополнение s1 является окрестностью x, то x принадлежит замыканию s2.

LaTeX

$$$ \\bigl(x \\in \\overline{\,s_1 \\cup s_2\} \\bigr) \\land (s_1^{\\complement} \\in \\mathcal{N}(x)) \\Rightarrow x \\in \\overline{s_2} $$$

Lean4

theorem mem_closure_of_mem_closure_union (h : x ∈ closure (s₁ ∪ s₂)) (h₁ : s₁ᶜ ∈ 𝓝 x) : x ∈ closure s₂ :=
  by
  rw [mem_closure_iff_nhds_ne_bot] at *
  rwa [← sup_principal, inf_sup_left, inf_principal_eq_bot.mpr h₁, bot_sup_eq] at h

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