nhds_σ — Mathlib

English

The index type of the neighborhood realizer is exactly the subtype of indices whose corresponding basic sets contain the point a.

Русский

Индексный тип реализатора окрестности точно является подтипом индексов, чьи базовые множества содержат точку a.

LaTeX

$$$ (F.nhds\ a).\sigma = \{ s : F.\sigma \mid a \in F.F s \} \quad\text{(as a subtype).}$$$

Lean4

@[simp]
theorem nhds_σ (F : Realizer α) (a : α) : (F.nhds a).σ = { s : F.σ // a ∈ F.F s } :=
  rfl

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