isEmbedding — Mathlib

English

If a map g: α → WeakBilin B satisfies that for every y ∈ F the function a ↦ B(g(a), y) is continuous, then g is continuous.

Русский

Если отображение g: α → WeakBilin B удовлетворяет условию, что для каждого y ∈ F функция a ↦ B(g(a), y) непрерывна, тогда g непрерывна.

LaTeX

$$continuous_of_continuous_eval [TopologicalSpace α] {g : α → WeakBilin B} (h : ∀ y, Continuous fun a => B (g a) y) : Continuous g$$

Lean4

/-- The coercion `(fun x y => B x y) : E → (F → 𝕜)` is an embedding. -/
theorem isEmbedding {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} (hB : Function.Injective B) :
    IsEmbedding fun (x : WeakBilin B) y => B x y :=
  Function.Injective.isEmbedding_induced <| LinearMap.coe_injective.comp hB

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