union_mem_nhds_of_mem_nhdsWithin — Mathlib

English

If L and R are neighborhoods of b within I₁ and I₂, respectively, and univ = I₁ ∪ I₂, then L ∪ R is a neighborhood of b.

Русский

Если L и R являются окрестностями точки b внутри I₁ и I₂, соответственно, и Univ = I₁ ∪ I₂, то L ∪ R является окрестностью b.

LaTeX

$$$$ (L \\cup R) \\in \\mathcal{N}(b) $$$$

Lean4

/-- If `L` and `R` are neighborhoods of `b` within sets whose union is `Set.univ`, then
`L ∪ R` is a neighborhood of `b`. -/
theorem union_mem_nhds_of_mem_nhdsWithin {b : α} {I₁ I₂ : Set α} (h : Set.univ = I₁ ∪ I₂) {L : Set α}
    (hL : L ∈ nhdsWithin b I₁) {R : Set α} (hR : R ∈ nhdsWithin b I₂) : L ∪ R ∈ nhds b :=
  by
  rw [← nhdsWithin_univ b, h, nhdsWithin_union]
  exact ⟨mem_of_superset hL (by simp), mem_of_superset hR (by simp)⟩

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