English
Let α be a topological space, a ∈ α, and s,t ⊆ α. If the convergence structure Ixx is compatible with both the neighborhood filter at a and the principal filters of s and t, then it is also compatible with the neighborhood filter restricted to s and the neighborhood filter restricted to t, respectively.
Русский
Пусть α — топологическое пространство, a ∈ α, и s, t ⊆ α. Если для некоторого класса сходимости Ixx выполняются совместимость с нормальными окрестностями a и с связями, порождаемыми множествами s и t, то аналогичная совместимость сохраняется для окрестностей s и t.
LaTeX
$$$TendstoIxxClass Ixx (\\mathcal{N}[s] a) (\\mathcal{N}[t] a).$$$
Lean4
instance tendstoIxxNhdsWithin {α : Type*} [TopologicalSpace α] (a : α) {s t : Set α} {Ixx}
[TendstoIxxClass Ixx (𝓝 a) (𝓝 a)] [TendstoIxxClass Ixx (𝓟 s) (𝓟 t)] : TendstoIxxClass Ixx (𝓝[s] a) (𝓝[t] a) :=
Filter.tendstoIxxClass_inf
