range_inr — Mathlib

English

The kernel of the first projection fst R M M2 equals the range of the right injection inr R M M2.

Русский

Ядро проекции fst равно образу правой инъекции inr.

LaTeX

$$$ \ker(\mathrm{fst}(R,M,M_2)) = \mathrm{range}(\mathrm{inr}(R,M,M_2)) $$$

Lean4

theorem range_inr : range (inr R M M₂) = ker (fst R M M₂) :=
  by
  ext x
  simp only [mem_ker, mem_range]
  constructor
  · rintro ⟨y, rfl⟩
    rfl
  · intro h
    exact ⟨x.snd, Prod.ext h.symm rfl⟩

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