ι_jointly_surjective — Mathlib

English

Equality of base points under injections ι i and ι j is equivalent to the glue relation Rel.

Русский

Равенство образов под инъекциями ι_i и ι_j эквивалентно отношению склейки Rel.

LaTeX

$$$(D.ι i).base\ x = (D.ι j).base\ y \;\iff\; D.Rel \langle i,x\rangle \langle j,y\rangle$$$

Lean4

theorem ι_jointly_surjective (x : 𝖣.glued.carrier) : ∃ (i : D.J) (y : (D.U i).carrier), (D.ι i).base y = x :=
  𝖣.ι_jointly_surjective forget x

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