ι_jointly_surjective — Mathlib

English

Every point in the glued space comes from some piece D.U i via ι i.

Русский

Каждый элемент слитого пространства получается как образ некоторого элемента из одного из компонентов D.U i через ι i.

LaTeX

$$$\forall x \in D.glued, \exists i, \exists y \in D.U_i, ι_i(y) = x.$$$

Lean4

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

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