proposition: Lemma equivoLR (W' : normedModType K) F (f g : T -> V) (h : T -> W') : f ~_F g -> [o_F f of h] =o_F g.
proof: Proof. by move/equiv_sym/equivoRL. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets functions) ereal reals signed topology normedtype prodnormedzmodule