mem_nhdsWithin_iff_exists_mem_nhds_inter

English

Equivalence of membership in nhdsWithin using nhds inter basis: t ∈ nhdsWithin a s iff ∃ u ∈ nhds a with u ∩ s ⊆ t.

Русский

Эквивалентность принадлежности t nhdsWithin a s через nhds: t ∈ nhdsWithin a s ⇔ ∃ u ∈ nhds a, u ∩ s ⊆ t.

LaTeX

$$$t ∈ 𝓝[a] s \iff ∃ u ∈ 𝓝 a, u ∩ s ⊆ t$$$

Lean4

theorem mem_nhdsWithin_iff_exists_mem_nhds_inter {t : Set α} {a : α} {s : Set α} : t ∈ 𝓝[s] a ↔ ∃ u ∈ 𝓝 a, u ∩ s ⊆ t :=
  (nhdsWithin_hasBasis (𝓝 a).basis_sets s).mem_iff

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