mkCLM_comp_outCLM — Mathlib

English

The composition mkCLM K E ∘L outCLM K E is the identity on SeparationQuotient E.

Русский

Составление mkCLM K E ∘L outCLM K E является тождественным отображением на SeparationQuotient E.

LaTeX

$$$(\mathrm{mkCLM}\ K\ E) \circ_L (\mathrm{outCLM}\ K\ E) = \mathrm{id}$$$

Lean4

@[simp]
theorem mkCLM_comp_outCLM : mkCLM K E ∘L outCLM K E = .id K (SeparationQuotient E) :=
  (exists_out_continuousLinearMap K E).choose_spec

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