include "formal_topology/basic_topologies.ma".
include "formal_topology/o-basic_topologies.ma".
include "formal_topology/relations_to_o-algebra.ma".
include "formal_topology/basic_topologies.ma".
include "formal_topology/o-basic_topologies.ma".
include "formal_topology/relations_to_o-algebra.ma".
definition o_basic_topology_of_basic_topology: basic_topology → Obasic_topology.
intros (b); constructor 1;
[ apply (POW' b) | apply (A b) | apply (J b);
definition o_basic_topology_of_basic_topology: basic_topology → Obasic_topology.
intros (b); constructor 1;
[ apply (POW' b) | apply (A b) | apply (J b);
lemma o_continuous_relation_of_continuous_relation_morphism :
∀S,T:category2_of_category1 BTop.
lemma o_continuous_relation_of_continuous_relation_morphism :
∀S,T:category2_of_category1 BTop.