extend_unique — Mathlib

English

Uniqueness of a conformal extension under dense embedding with isUniformInducing.

Русский

Единственность конформного продолжения при плотном вложении и изотр. индукции.

LaTeX

$$$\\text{extend_unique}(f,e,h\\_dense,h\\_e) = g \\Rightarrow \\dots$$$

Lean4

theorem extend_unique (g : Fₗ →SL[σ₁₂] F) (H : g.comp e = f) : extend f e h_dense h_e = g :=
  ContinuousLinearMap.coeFn_injective <|
    uniformly_extend_unique h_e h_dense (ContinuousLinearMap.ext_iff.1 H) g.continuous

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