English
For a finite index set I, the nhds within pi-space equals an infimum expressed via coordinate projections and principal filters.
Русский
Для конечного индекса I окрестность внутри пространства π-типа равна инфимума через проекции координат и главные фильтры.
LaTeX
$$$$ 𝓝_{\\pi I s} x = \\left( \\bigwedge_{i \\in I} \\mathrm{comap}(\\lambda x . x_i)( 𝓝(x_i) ) \\right) \\wedge \\left( \\bigwedge_{i \\notin I} \\mathrm{comap}(\\lambda x . x_i)( 𝓝(x_i) ) \\right) $$$$
Lean4
theorem nhdsWithin_pi_eq {I : Set ι} (hI : I.Finite) (s : ∀ i, Set (X i)) (x : ∀ i, X i) :
𝓝[pi I s] x = (⨅ i ∈ I, comap (fun x => x i) (𝓝[s i] x i)) ⊓ ⨅ (i) (_ : i ∉ I), comap (fun x => x i) (𝓝 (x i)) :=
by
simp only [nhdsWithin, nhds_pi, Filter.pi, pi_def, ← iInf_principal_finite hI, comap_inf, comap_principal]
rw [iInf_split _ fun i => i ∈ I, inf_right_comm]
simp only [iInf_inf_eq]
