isEmbedding_inducingFn — Mathlib

English

Under a separating dual assumption, inducingFn is an embedding (injective and topologically embedding).

Русский

При предположении существования разделяющего двойственного, inducingFn является вложением (инъективным и топологически вложенным).

LaTeX

$$$\\text{IsEmbedding}(\\operatorname{inducingFn})$$$

Lean4

theorem isEmbedding_inducingFn [SeparatingDual 𝕜 F] : IsEmbedding (inducingFn 𝕜 E F) :=
  by
  refine Function.Injective.isEmbedding_induced fun A B hAB => ?_
  rw [ContinuousLinearMapWOT.ext_dual_iff]
  simpa [funext_iff] using hAB

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