inl_snd — Mathlib

English

The exactness of inr and fst is a basic example of a direct sum decomposition.

Русский

Точность inr и fst — базовый пример разложения в прямую сумму.

LaTeX

$$$$ \\operatorname{Exact}(\\mathrm{inr},\\mathrm{fst}). $$$$

Lean4

theorem inl_snd : Function.Exact (LinearMap.inl R M N) (LinearMap.snd R M N) :=
  by
  rintro ⟨x, y⟩
  simp only [LinearMap.snd_apply, @eq_comm _ y, LinearMap.coe_inl, Set.mem_range, Prod.mk.injEq, exists_eq_left]

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