Rel — Mathlib

English

Each inclusion ι_i is injective; distinct points from the i-th piece map to distinct points in the glued space.

Русский

Каждое вложение ι_i инъективно; разные точки из компоненты i остаются различными после склейки.

LaTeX

$$$\forall i, \text{ι}_i \text{ is injective}$$$

Lean4

/-- An equivalence relation on `Σ i, D.U i` that holds iff `𝖣.ι i x = 𝖣.ι j y`.
See `TopCat.GlueData.ι_eq_iff_rel`.
-/
def Rel (a b : Σ i, ((D.U i : TopCat) : Type _)) : Prop :=
  ∃ x : D.V (a.1, b.1), D.f _ _ x = a.2 ∧ D.f _ _ (D.t _ _ x) = b.2

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