Definition. We define struct_c_Hausdorff_topology to be λX ⇒ struct_c X ∧ unpack_c_o X (λX' Open ⇒ Open (λx ⇒ x ∈ X') ∧ (∀U V : set → prop, Open U → Open V → Open (λx ⇒ U x ∧ U x)) ∧ (∀C : (set → prop) → prop, (∀U : set → prop, C U → Open U) → Open (λx ⇒ ∃U : set → prop, C U ∧ U x)) ∧ (∀a b ∈ X', a ≠ b → ∃U V : set → prop, Open U ∧ Open V ∧ U a ∧ V b ∧ (∀x, U x → ¬ V x))) of type set → prop.

In Proofgold the corresponding term root is af0970... and object id is e61511...

L13

Theorem. (MetaCat_struct_c_Hausdorff_topology)

MetaCat struct_c_Hausdorff_topology Hom_struct_c struct_id struct_comp

In Proofgold the corresponding term root is 39da15... and proposition id is 2bba3b...

Proof:
Proof not loaded.

L19

Theorem. (MetaCat_struct_c_Hausdorff_topology_Forgetful)

MetaFunctor struct_c_Hausdorff_topology Hom_struct_c struct_id struct_comp (λ_ ⇒ True) SetHom (λX ⇒ lam_id X) (λX Y Z f g ⇒ (lam_comp X f g)) (λX ⇒ X 0) (λX Y f ⇒ f)

In Proofgold the corresponding term root is c97e7b... and proposition id is dd73c1...

Proof:
Proof not loaded.

L29

Proposition. (MetaCat_struct_c_Hausdorff_topology_initial)

∃Y : set, ∃uniqa : set → set, initial_p struct_c_Hausdorff_topology Hom_struct_c struct_id struct_comp Y uniqa

In Proofgold the corresponding term root is c6af43... and proposition id is 28373d...

Proof:
Proof not loaded.

L33

Proposition. (MetaCat_struct_c_Hausdorff_topology_terminal)

∃Y : set, ∃uniqa : set → set, terminal_p struct_c_Hausdorff_topology Hom_struct_c struct_id struct_comp Y uniqa

In Proofgold the corresponding term root is 3d6cf9... and proposition id is 3bc025...

Proof:
Proof not loaded.

L37

Proposition. (MetaCat_struct_c_Hausdorff_topology_coproduct_constr)

∃coprod : set → set → set, ∃i0 i1 : set → set → set, ∃copair : set → set → set → set → set → set, coproduct_constr_p struct_c_Hausdorff_topology Hom_struct_c struct_id struct_comp coprod i0 i1 copair

In Proofgold the corresponding term root is 5b67a9... and proposition id is 393181...

Proof:
Proof not loaded.

L44

Proposition. (MetaCat_struct_c_Hausdorff_topology_product_constr)

∃prod : set → set → set, ∃pi0 pi1 : set → set → set, ∃pair : set → set → set → set → set → set, product_constr_p struct_c_Hausdorff_topology Hom_struct_c struct_id struct_comp prod pi0 pi1 pair

In Proofgold the corresponding term root is defa7f... and proposition id is 036877...

Proof:
Proof not loaded.

L51

Proposition. (MetaCat_struct_c_Hausdorff_topology_coequalizer_constr)

∃quot : set → set → set → set → set, ∃canonmap : set → set → set → set → set, ∃fac : set → set → set → set → set → set → set, coequalizer_constr_p struct_c_Hausdorff_topology Hom_struct_c struct_id struct_comp quot canonmap fac

In Proofgold the corresponding term root is 09c43e... and proposition id is 62158c...

Proof:
Proof not loaded.

L58

Proposition. (MetaCat_struct_c_Hausdorff_topology_equalizer_constr)

∃quot : set → set → set → set → set, ∃canonmap : set → set → set → set → set, ∃fac : set → set → set → set → set → set → set, equalizer_constr_p struct_c_Hausdorff_topology Hom_struct_c struct_id struct_comp quot canonmap fac

In Proofgold the corresponding term root is fd2df2... and proposition id is fcf6b3...

Proof:
Proof not loaded.

L65

Proposition. (MetaCat_struct_c_Hausdorff_topology_pushout_constr)

∃po : set → set → set → set → set → set, ∃i0 : set → set → set → set → set → set, ∃i1 : set → set → set → set → set → set, ∃copair : set → set → set → set → set → set → set → set → set, pushout_constr_p struct_c_Hausdorff_topology Hom_struct_c struct_id struct_comp po i0 i1 copair

In Proofgold the corresponding term root is a0f8b9... and proposition id is d648e4...

Proof:
Proof not loaded.

L73

Proposition. (MetaCat_struct_c_Hausdorff_topology_pullback_constr)

∃pb : set → set → set → set → set → set, ∃pi0 : set → set → set → set → set → set, ∃pi1 : set → set → set → set → set → set, ∃pair : set → set → set → set → set → set → set → set → set, pullback_constr_p struct_c_Hausdorff_topology Hom_struct_c struct_id struct_comp pb pi0 pi1 pair

In Proofgold the corresponding term root is baca17... and proposition id is 59f337...

Proof:
Proof not loaded.

L81

Proposition. (MetaCat_struct_c_Hausdorff_topology_product_exponent)

∃prod : set → set → set, ∃pi0 pi1 : set → set → set, ∃pair : set → set → set → set → set → set, ∃exp : set → set → set, ∃a : set → set → set, ∃lm : set → set → set → set → set, product_exponent_constr_p struct_c_Hausdorff_topology Hom_struct_c struct_id struct_comp prod pi0 pi1 pair exp a lm

In Proofgold the corresponding term root is 568d6e... and proposition id is c8e85c...

Proof:
Proof not loaded.

L91

Proposition. (MetaCat_struct_c_Hausdorff_topology_subobject_classifier)

∃one : set, ∃uniqa : set → set, ∃Omega : set, ∃tru : set, ∃ch : set → set → set → set, ∃constr : set → set → set → set → set → set → set, subobject_classifier_p struct_c_Hausdorff_topology Hom_struct_c struct_id struct_comp one uniqa Omega tru ch constr

In Proofgold the corresponding term root is 593fae... and proposition id is e10966...

Proof:
Proof not loaded.

L99

Proposition. (MetaCat_struct_c_Hausdorff_topology_nno)

∃one : set, ∃uniqa : set → set, ∃N : set, ∃zer suc : set, ∃rec : set → set → set → set, nno_p struct_c_Hausdorff_topology Hom_struct_c struct_id struct_comp one uniqa N zer suc rec

In Proofgold the corresponding term root is f01e4a... and proposition id is 71b81c...

Proof:
Proof not loaded.

L108

Proposition. (MetaCat_struct_c_Hausdorff_topology_left_adjoint_forgetful)

∃F0 : set → set, ∃F1 : set → set → set → set, ∃eta eps : set → set, MetaAdjunction_strict (λ_ ⇒ True) SetHom (λX ⇒ (lam_id X)) (λX Y Z f g ⇒ (lam_comp X f g)) struct_c_Hausdorff_topology Hom_struct_c struct_id struct_comp F0 F1 (λX ⇒ X 0) (λX Y f ⇒ f) eta eps

In Proofgold the corresponding term root is 14e059... and proposition id is b66fd9...

Proof:
Proof not loaded.