English
For a family of topological spaces {X_i} indexed by i, the evaluation map at i, from the product ∏_j X_j to X_i, is an open map.
Русский
Для семейства топологических пространств {X_i}, индексируемого i, отображение выбора координаты i из произведения ∏_j X_j на X_i является открытым отображением.
LaTeX
$$$\mathrm{IsOpenMap}(\pi_i)$ where $\pi_i: \prod_j X_j \to X_i$ is the projection onto the i-th coordinate$$
Lean4
theorem isOpenMap_eval (i : ι) : IsOpenMap (Function.eval i : (∀ i, X i) → X i) := by
classical
refine (isTopologicalBasis_pi fun _ ↦ isTopologicalBasis_opens).isOpenMap_iff.2 ?_
rintro _ ⟨U, s, hU, rfl⟩
obtain h | h := ((s : Set ι).pi U).eq_empty_or_nonempty
· simp [h]
by_cases hi : i ∈ s
· rw [eval_image_pi (mod_cast hi) h]
exact hU _ hi
· rw [eval_image_pi_of_notMem (mod_cast hi), if_pos h]
exact isOpen_univ
