continuous_coinducingCoprod — Mathlib

English

For every S and x ∈ X(S), the map a ↦ coinducingCoprod ⟨⟨S,x⟩, a⟩ is continuous.

Русский

Для каждого S и x ∈ X(S) отображение a ↦ coinducingCoprod ⟨⟨S,x⟩, a⟩ непрерывно.

LaTeX

$$$\text{Continuous}\;\bigl( a \mapsto X.coinducingCoprod\langle\langle S,x\rangle, a\rangle\bigr).$$$

Lean4

theorem continuous_coinducingCoprod {S : LightProfinite.{u}} (x : X.val.obj ⟨S⟩) :
    Continuous fun a ↦ (X.coinducingCoprod ⟨⟨S, x⟩, a⟩) :=
  by
  suffices ∀ (i : (T : LightProfinite.{u}) × X.val.obj ⟨T⟩), Continuous (fun (a : i.fst) ↦ X.coinducingCoprod ⟨i, a⟩)
    from this ⟨_, _⟩
  rw [← continuous_sigma_iff]
  apply continuous_coinduced_rng

Похожие утверждения