ι_jointly_surjective — Mathlib

English

Every point of the glued space arises from some chart U_i, i.e., there exist i in D.J and y in D.U_i with (ι_i).base y = x for any x in 𝖣.glued.

Русский

Каждая точка слитого пространства восходит к некоторому открытому множеству U_i, существует i и y с (ι_i).base y = x.

LaTeX

$$$\exists i \in D.J, \exists y \in D.U_i, (\mathcal{ι}_i)_{base}(y) = x$$$

Lean4

theorem ι_jointly_surjective (x : 𝖣.glued) : ∃ (i : D.J) (y : D.U i), (𝖣.ι i).base y = x :=
  𝖣.ι_jointly_surjective (PresheafedSpace.forget _ ⋙ CategoryTheory.forget TopCat) x

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