sigmaIsoHom_inj — Mathlib

English

The map sigmaIsoHom f from the disjoint union fiber product to S is injective.

Русский

Отображение sigmaIsoHom f инъективно.

LaTeX

$$$$\sigmaIsoHom_f\;\text{ is injective.}$$$$

Lean4

theorem sigmaIsoHom_inj : Function.Injective (sigmaIsoHom f) :=
  by
  rintro ⟨⟨_, _, rfl⟩, ⟨_, hx⟩⟩ ⟨⟨_, _, rfl⟩, ⟨_, hy⟩⟩ h
  refine Sigma.subtype_ext ?_ h
  simp only [sigmaIsoHom_apply] at h
  rw [Set.mem_preimage, Set.mem_singleton_iff] at hx hy
  simp [← hx, ← hy, h]

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