English
If every T_i is a topological basis, then the infimum of induced topologies yields a basis described by finite intersections of inverse images.
Русский
Если каждый T_i является базисом, то инфимум индуцированных топологий образует базис, задаваемый конечными пересечениями обратных изображений.
LaTeX
$$$\\forall i,\\mathsf{IsTopologicalBasis}(T_i) \\to \\mathsf{IsTopologicalBasis}\\left(\\text{t := } \\bigwedge_i \\operatorname{induced}(f_i)(t_i)\\right)\\;\\{S \\mid \\exists (U: \\forall i, Set(X_i)) (F: Finset ι), (\\forall i, i\\in F \\to U_i \\in T_i) \\wedge S = \\bigcap_{i\\in F} f_i^{-1}'(U_i)\\}$$$
Lean4
theorem iInf_induced {β : Type*} {ι : Type*} {X : ι → Type*} [t : Π i, TopologicalSpace (X i)]
{T : Π i, Set (Set (X i))} (cond : ∀ i, IsTopologicalBasis (T i)) (f : Π i, β → X i) :
IsTopologicalBasis (t := ⨅ i, induced (f i) (t i))
{S | ∃ (U : ∀ i, Set (X i)) (F : Finset ι), (∀ i, i ∈ F → U i ∈ T i) ∧ S = ⋂ (i) (_ : i ∈ F), f i ⁻¹' U i} :=
by
convert IsTopologicalBasis.iInf (fun i ↦ (cond i).induced (f i)) with S
constructor <;> rintro ⟨U, F, hUT, hSU⟩
· exact ⟨fun i ↦ (f i) ⁻¹' (U i), F, fun i hi ↦ mem_image_of_mem _ (hUT i hi), hSU⟩
· choose! U' hU' hUU' using hUT
exact ⟨U', F, hU', hSU ▸ (.symm <| iInter₂_congr hUU')⟩
