English
A simplified, symmetric variant of continuous_dom_pi, expressing a canonical equality of maps under pi-limits.
Русский
Упрощённая симметричная версия, равенство отображений в рамках произведения по точкам.
LaTeX
$$$\\text{Eq}(\\text{Continuous f}, \\text{Continuous across pi})$$$
Lean4
/-- A finitary (instead of binary) version of `continuous_dom_prod`. -/
theorem continuous_dom_pi {n : Type*} [Finite n] {X : Type*} [TopologicalSpace X] {A : n → ι → Type*}
[∀ j i, TopologicalSpace (A j i)] {C : (j : n) → (i : ι) → Set (A j i)} (hCopen : ∀ j i, IsOpen (C j i))
{f : (Π j : n, Πʳ i : ι, [A j i, C j i]) → X} :
Continuous f ↔ ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S), Continuous (f ∘ Pi.map fun _ ↦ inclusion _ _ hS) :=
by
refine ⟨by fun_prop, fun H ↦ ?_⟩
simp_rw [continuous_iff_continuousAt, ContinuousAt]
intro x
set S : Set ι := {i | ∀ j, x j i ∈ C j i}
have hS : cofinite ≤ 𝓟 S := by
rw [le_principal_iff]
change ∀ᶠ i in cofinite, ∀ j : n, x j i ∈ C j i
simp [-eventually_cofinite]
let x' (j : n) : Πʳ i : ι, [A j i, C j i]_[𝓟 S] := .mk (fun i ↦ x j i) (fun i hi ↦ hi _)
have hxx' : Pi.map (fun j ↦ inclusion _ _ hS) x' = x := rfl
simp_rw [← hxx', nhds_pi, Pi.map_apply, nhds_eq_map_inclusion (hCopen _), ← map_piMap_pi_finite, tendsto_map'_iff, ←
nhds_pi]
exact (H _ _).tendsto _
