nhdsWithin_basis_open — Mathlib

English

Basis for nhdsWithin with open sets: (𝓝[t] a) HasBasis (a ∈ u ∧ IsOpen u) (u ∩ t).

Русский

База для nhdsWithin с открытыми множествами: имеет базис a ∈ u и IsOpen u над u ∩ t.

LaTeX

$$$(nhdsWithin a t).HasBasis (fun u => a ∈ u ∧ IsOpen u) (fun u => u ∩ t)$$$

Lean4

theorem nhdsWithin_basis_open (a : α) (t : Set α) : (𝓝[t] a).HasBasis (fun u => a ∈ u ∧ IsOpen u) fun u => u ∩ t :=
  nhdsWithin_hasBasis (nhds_basis_opens a) t

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