fromOpenSubsetsGlue_injective — Mathlib

English

The map fromOpenSubsetsGlue is injective on open cover data, i.e., different elements yield different glued points.

Русский

Отображение fromOpenSubsetsGlue инъективно: разные элементы дают разные точки склейки.

LaTeX

$$fromOpenSubsetsGlue is injective$$

Lean4

theorem fromOpenSubsetsGlue_injective : Function.Injective (fromOpenSubsetsGlue U) :=
  by
  intro x y e
  obtain ⟨i, ⟨x, hx⟩, rfl⟩ := (ofOpenSubsets U).ι_jointly_surjective x
  obtain ⟨j, ⟨y, hy⟩, rfl⟩ := (ofOpenSubsets U).ι_jointly_surjective y
  rw [ι_fromOpenSubsetsGlue_apply, ι_fromOpenSubsetsGlue_apply] at e
  subst e
  rw [(ofOpenSubsets U).ι_eq_iff_rel]
  exact ⟨⟨⟨x, hx⟩, hy⟩, rfl, rfl⟩

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