proposition: Lemma topologydirprod_imply : ∏ x : U × V, isfilter_imply (topologydirprod x).
proof: Proof. intros x A B H. apply hinhfun. intros AB. exists (pr1 AB), (pr1 (pr2 AB)) ; split ; [ | split]. - exact (pr1 (pr2 (pr2 AB))). - exact (pr1 (pr2 (pr2 (pr2 AB)))). - intros x' y' Hx' Hy'. now apply H, (pr2 (pr2 (pr2 (pr2 AB)))). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Topology.Filters UniMath.Algebra.Groups UniMath.Algebra.DivisionRig UniMath.Algebra.ConstructiveStructures