M : Type u_2
N✝ : Type ?u.479189
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N✝
N : Type u_1
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (s : M), s ∈ S → ↑f s = 0
fb : NormNoninc f
x : M ⧸ S
fb' : ‖f‖ ≤ ↑1
⊢ ‖↑(lift S f hf) x‖ ≤ ‖x‖
M : Type u_2
N✝ : Type ?u.479189
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N✝
N : Type u_1
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (s : M), s ∈ S → ↑f s = 0
fb : NormNoninc f
x : M ⧸ S
⊢ ‖↑(lift S f hf) x‖ ≤ ‖x‖
have fb' : ‖f‖ ≤ (1 : ℝ≥0) := NormNoninc.normNoninc_iff_norm_le_one.mp fb
no goals
M : Type u_2
N✝ : Type ?u.479189
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N✝
N : Type u_1
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (s : M), s ∈ S → ↑f s = 0
fb : NormNoninc f
x : M ⧸ S
fb' : ‖f‖ ≤ ↑1
⊢ ‖↑(lift S f hf) x‖ ≤ ‖x‖
simpa using le_of_opNorm_le _ (f.lift_norm_le _ _ fb') _