English
The equality of the base images under ι is equivalent to the relational condition Rel between indices and points.
Русский
Равенство образов под ι эквивалентно отношению Rel между индексами и точками.
LaTeX
$$$(D.ι i).base x = (D.ι j).base y \iff D.Rel \langle i,x \rangle \langle j,y \rangle$$$
Lean4
theorem ι_eq_iff (i j : D.J) (x : (D.U i).carrier) (y : (D.U j).carrier) :
(𝖣.ι i).base x = (𝖣.ι j).base y ↔ D.Rel ⟨i, x⟩ ⟨j, y⟩ :=
by
refine
Iff.trans ?_
(TopCat.GlueData.ι_eq_iff_rel
D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData i j x y)
rw [← ((TopCat.mono_iff_injective D.isoCarrier.inv).mp _).eq_iff, ← ConcreteCategory.comp_apply]
· simp_rw [← D.ι_isoCarrier_inv]
rfl -- `rfl` was not needed before https://github.com/leanprover-community/mathlib4/pull/13170
· infer_instance
