English
Let (α_i) be a family of preordered spaces each with a topology and OrderTopology. For a function f assigning to each i an element f(i) in α_i, the class TendstoIxx for the interval Icc is compatible at the product neighborhood 𝓝 f with itself.
Русский
Пусть имеется семейство предпорядковых пространств (α_i) с топологией и OrderTopology. Для отображения f, сопоставляющего каждому i элемент в α_i, класс TendstoIxx для интервала Icc совместим в произведении с itself на 𝓝 f.
LaTeX
$$$TendstoIxxClass Icc (\\mathcal{N} f) (\\mathcal{N} f).$$$
Lean4
instance tendstoIccClassNhdsPi {ι : Type*} {α : ι → Type*} [∀ i, Preorder (α i)] [∀ i, TopologicalSpace (α i)]
[∀ i, OrderTopology (α i)] (f : ∀ i, α i) : TendstoIxxClass Icc (𝓝 f) (𝓝 f) :=
by
constructor
conv in (𝓝 f).smallSets => rw [nhds_pi, Filter.pi]
simp only [smallSets_iInf, smallSets_comap_eq_comap_image, tendsto_iInf, tendsto_comap_iff]
intro i
have : Tendsto (fun g : ∀ i, α i => g i) (𝓝 f) (𝓝 (f i)) := (continuous_apply i).tendsto f
refine (this.comp tendsto_fst).Icc (this.comp tendsto_snd) |>.smallSets_mono ?_
filter_upwards [] using fun ⟨f, g⟩ ↦ image_subset_iff.mpr fun p hp ↦ ⟨hp.1 i, hp.2 i⟩
