exists_subset_of_mem_open — Mathlib

English

If a point a lies in an open set u, then there exists a basis element v ∈ B with a ∈ v ⊆ u.

Русский

Если a ∈ u и u открыто, то существует элемент базы v ∈ B такой, что a ∈ v ⊆ u.

LaTeX

$$exists_subset_of_mem_open {b : Set (Set α)} (hb : IsTopologicalBasis b) {a : α} {u : Set α} (au : a ∈ u) (ou : IsOpen u) : ∃ v ∈ b, a ∈ v ∧ v ⊆ u$$

Lean4

theorem exists_subset_of_mem_open {b : Set (Set α)} (hb : IsTopologicalBasis b) {a : α} {u : Set α} (au : a ∈ u)
    (ou : IsOpen u) : ∃ v ∈ b, a ∈ v ∧ v ⊆ u :=
  hb.mem_nhds_iff.1 <| IsOpen.mem_nhds ou au

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