restrictDom_comp_subtype — Mathlib

English

The composition of restrictDom with the subtype embedding is the identity on the appropriate domain.

Русский

Состав restrictDom и вложение подмодуля-типa является тождественным отображением на соответствующем домене.

LaTeX

$$$\bigl(\mathrm{restrictDom}(M,R,s)\bigr)\;\circ\; (\mathrm{Submodule}.\mathrm{subtype} _) = \mathrm{LinearMap}.id$$$

Lean4

theorem restrictDom_comp_subtype (s : Set α) [DecidablePred (· ∈ s)] :
    (restrictDom M R s).comp (Submodule.subtype _) = LinearMap.id :=
  by
  ext l a
  by_cases h : a ∈ s
  · simp [h]
  simpa [h] using ((mem_supported' R l.1).1 l.2 a h).symm

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