exists_nonempty_subset — Mathlib

English

If u is a nonempty open set, then there exists a basis element v ∈ B with v ⊆ u and v is nonempty.

Русский

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

LaTeX

$$$\exists v \in B,\ v\neq \varnothing \land v \subseteq u.$$$

Lean4

theorem exists_nonempty_subset {B : Set (Set α)} (hb : IsTopologicalBasis B) {u : Set α} (hu : u.Nonempty)
    (ou : IsOpen u) : ∃ v ∈ B, Set.Nonempty v ∧ v ⊆ u :=
  let ⟨x, hx⟩ := hu
  let ⟨v, vB, xv, vu⟩ := hb.exists_subset_of_mem_open hx ou
  ⟨v, vB, ⟨x, xv⟩, vu⟩

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