proposition: Lemma Theta_sym (F : filter_on T) (f g : T -> V) : (f =Theta_F g) = (g =Theta_F f).
proof: Proof. by rewrite !eqThetaE propeqE !bigThetaE !eqOmegaO; split => -[]. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets functions) ereal reals signed topology normedtype prodnormedzmodule