embeddingPiTangent_injOn — Mathlib

English

The embedding map on the bump covering is injective on the domain s.

Русский

Встраивание по покрытию-бампингу инъективно на области s.

LaTeX

$$$\text{InjOn}(f.embeddingPiTangent\,s)$$$

Lean4

theorem embeddingPiTangent_injOn : InjOn f.embeddingPiTangent s :=
  by
  intro x hx y _ h
  simp only [embeddingPiTangent_coe, funext_iff] at h
  obtain ⟨h₁, h₂⟩ := Prod.mk_inj.1 (h (f.ind x hx))
  rw [f.apply_ind x hx] at h₂
  rw [← h₂, f.apply_ind x hx, one_smul, one_smul] at h₁
  have := f.mem_extChartAt_source_of_eq_one h₂.symm
  exact (extChartAt I (f.c _)).injOn (f.mem_extChartAt_ind_source x hx) this h₁

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