nhds_F — Mathlib

English

For the neighborhood realizer, the F-component on an index s is the original F-value at the underlying s, i.e. (F.nhds a).F(s) = F.F(s.1).

Русский

Для окрестностенного реализатора компонент F на индексе s равен исходному значению F на основанном s. то есть (F.nhds a).F(s) = F.F(s.1).

LaTeX

$$$ (F.nhds a).F s = F.F (s.1). $$$$

Lean4

@[simp]
theorem nhds_F (F : Realizer α) (a : α) (s) : (F.nhds a).F s = F.F s.1 :=
  rfl

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