English
If M and A form a monoid with a distributive multiplicative action, then SeparationQuotient A inherits a MulDistribMulAction.
Русский
Если M и A образуют моноид с распределимым действием умножения, то SeparationQuotient A наследует MulDistribMulAction.
LaTeX
$$$\mathrm{MulDistribMulAction}\ M (\mathrm{SeparationQuotient} A)$$$
Lean4
/-- There exists a continuous `K`-linear map from `SeparationQuotient E` to `E`
such that `mk (outCLM x) = x` for all `x`.
Note that continuity of this map comes for free, because `mk` is a topology inducing map.
-/
theorem exists_out_continuousLinearMap :
∃ f : SeparationQuotient E →L[K] E, mkCLM K E ∘L f = .id K (SeparationQuotient E) :=
by
rcases (mkCLM K E).toLinearMap.exists_rightInverse_of_surjective (LinearMap.range_eq_top.mpr surjective_mk) with
⟨f, hf⟩
replace hf : mk ∘ f = id := congr_arg DFunLike.coe hf
exact ⟨⟨f, isInducing_mk.continuous_iff.2 (by continuity)⟩, DFunLike.ext' hf⟩
