lift_unique — Mathlib

English

If a normed map g on the quotient composed with the projection equals f, then g is exactly the lift of f.

Русский

Если $g\\circ \\pi_S = f$, то $g$ является единственным лифтом $f$.

LaTeX

$$$g \\circ S.normedMk = f \\Rightarrow g = lift S f hf$$$

Lean4

theorem lift_unique {N : Type*} [SeminormedAddCommGroup N] (S : AddSubgroup M) (f : NormedAddGroupHom M N)
    (hf : ∀ s ∈ S, f s = 0) (g : NormedAddGroupHom (M ⧸ S) N) (h : g.comp S.normedMk = f) : g = lift S f hf :=
  by
  ext x
  rcases AddSubgroup.surjective_normedMk _ x with ⟨x, rfl⟩
  change g.comp S.normedMk x = _
  simp only [h]
  rfl

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