mem_nhdsWithin — Mathlib

English

Characterization of membership in nhdsWithin: t ∈ nhdsWithin a s iff ∃ open u with a ∈ u and u ∩ s ⊆ t.

Русский

Характеризация принадлежности t окрестности внутри s: t ∈ nhdsWithin a s тогда и только если существует открытое u с a ∈ u и u ∩ s ⊆ t.

LaTeX

$$$t \in 𝓝[s] a \iff \exists u, IsOpen u ∧ a ∈ u ∧ u \cap s \subseteq t$$$

Lean4

theorem mem_nhdsWithin {t : Set α} {a : α} {s : Set α} : t ∈ 𝓝[s] a ↔ ∃ u, IsOpen u ∧ a ∈ u ∧ u ∩ s ⊆ t := by
  simpa only [and_assoc, and_left_comm] using (nhdsWithin_basis_open a s).mem_iff

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