sumCongrHom_injective — Mathlib

English

The map sumCongrHom α β is injective; i.e., sumCongr uniquely determines its pair of components.

Русский

Отображение sumCongrHom α β инъективно; то есть суммаCongr однозначно восстанавливает пару компонент.

LaTeX

$$$$\\\\text{Injective}(\\\\mathrm{sumCongrHom}_{\\\\alpha\\\\beta}).$$$$

Lean4

theorem sumCongrHom_injective {α β : Type*} : Function.Injective (sumCongrHom α β) :=
  by
  rintro ⟨⟩ ⟨⟩ h
  rw [Prod.mk_inj]
  constructor <;> ext i
  · simpa using Equiv.congr_fun h (Sum.inl i)
  · simpa using Equiv.congr_fun h (Sum.inr i)

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