We will prove ¬ regular_space R_K R_K_topology.
Assume Hreg: regular_space R_K R_K_topology.
We will prove False.
We prove the intermediate claim HregSep: ∀x : set, x ∈ R_K → ∀F : set, closed_in R_K R_K_topology F → x ∉ F → ∃U V : set, U ∈ R_K_topology ∧ V ∈ R_K_topology ∧ x ∈ U ∧ F ⊆ V ∧ U ∩ V = Empty.
An exact proof term for the current goal is (andER (one_point_sets_closed R_K R_K_topology) (∀x : set, x ∈ R_K → ∀F : set, closed_in R_K R_K_topology F → x ∉ F → ∃U V : set, U ∈ R_K_topology ∧ V ∈ R_K_topology ∧ x ∈ U ∧ F ⊆ V ∧ U ∩ V = Empty) Hreg).
We prove the intermediate claim HKsubX: K_set ⊆ R_K.
Let t be given.
Assume Ht: t ∈ K_set.
An exact proof term for the current goal is (K_set_Subq_R t Ht).
We prove the intermediate claim HTx: topology_on R_K R_K_topology.
An exact proof term for the current goal is (regular_space_topology_on R_K R_K_topology Hreg).
We prove the intermediate claim HKclosed: closed_in R_K R_K_topology K_set.
rewrite the current goal using (closure_of_K_in_R_K_topology) (from right to left) at position 1.
An exact proof term for the current goal is (closure_is_closed R_K R_K_topology K_set HTx HKsubX).
We prove the intermediate claim H0X: 0 ∈ R_K.
An exact proof term for the current goal is real_0.
We prove the intermediate claim H0notK: 0 ∉ K_set.
An exact proof term for the current goal is zero_not_in_K_set.
We prove the intermediate claim HexUV: ∃U V : set, U ∈ R_K_topology ∧ V ∈ R_K_topology ∧ 0 ∈ U ∧ K_set ⊆ V ∧ U ∩ V = Empty.
An exact proof term for the current goal is (HregSep 0 H0X K_set HKclosed H0notK).
Apply HexUV to the current goal.
Let U be given.
Assume HexV: ∃V : set, U ∈ R_K_topology ∧ V ∈ R_K_topology ∧ 0 ∈ U ∧ K_set ⊆ V ∧ U ∩ V = Empty.
Apply HexV to the current goal.
Let V be given.
Assume HUV.
We prove the intermediate claim Hpre: (((U ∈ R_K_topology ∧ V ∈ R_K_topology) ∧ 0 ∈ U) ∧ K_set ⊆ V).
An exact proof term for the current goal is (andEL (((U ∈ R_K_topology ∧ V ∈ R_K_topology) ∧ 0 ∈ U) ∧ K_set ⊆ V) (U ∩ V = Empty) HUV).
We prove the intermediate claim Hdisj: U ∩ V = Empty.
An exact proof term for the current goal is (andER (((U ∈ R_K_topology ∧ V ∈ R_K_topology) ∧ 0 ∈ U) ∧ K_set ⊆ V) (U ∩ V = Empty) HUV).
We prove the intermediate claim Hpre2: (U ∈ R_K_topology ∧ V ∈ R_K_topology) ∧ 0 ∈ U.
An exact proof term for the current goal is (andEL ((U ∈ R_K_topology ∧ V ∈ R_K_topology) ∧ 0 ∈ U) (K_set ⊆ V) Hpre).
We prove the intermediate claim HKsubV: K_set ⊆ V.
An exact proof term for the current goal is (andER ((U ∈ R_K_topology ∧ V ∈ R_K_topology) ∧ 0 ∈ U) (K_set ⊆ V) Hpre).
We prove the intermediate claim HUVopen: U ∈ R_K_topology ∧ V ∈ R_K_topology.
An exact proof term for the current goal is (andEL (U ∈ R_K_topology ∧ V ∈ R_K_topology) (0 ∈ U) Hpre2).
We prove the intermediate claim H0U: 0 ∈ U.
An exact proof term for the current goal is (andER (U ∈ R_K_topology ∧ V ∈ R_K_topology) (0 ∈ U) Hpre2).
We prove the intermediate claim HUopen: U ∈ R_K_topology.
An exact proof term for the current goal is (andEL (U ∈ R_K_topology) (V ∈ R_K_topology) HUVopen).
We prove the intermediate claim HVopen: V ∈ R_K_topology.
An exact proof term for the current goal is (andER (U ∈ R_K_topology) (V ∈ R_K_topology) HUVopen).
Set B to be the term (R_standard_basis ∪ R_K_basis).
We prove the intermediate claim HUprop: ∀x ∈ U, ∃b0 ∈ B, x ∈ b0 ∧ b0 ⊆ U.
An exact proof term for the current goal is (SepE2 (𝒫 R_K) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b0 ∈ B, x0 ∈ b0 ∧ b0 ⊆ U0) U HUopen).
We prove the intermediate claim HVprop: ∀x ∈ V, ∃b0 ∈ B, x ∈ b0 ∧ b0 ⊆ V.
An exact proof term for the current goal is (SepE2 (𝒫 R_K) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b0 ∈ B, x0 ∈ b0 ∧ b0 ⊆ U0) V HVopen).
We prove the intermediate claim HexbU: ∃bU ∈ B, 0 ∈ bU ∧ bU ⊆ U.
An exact proof term for the current goal is (HUprop 0 H0U).
Apply HexbU to the current goal.
Let bU be given.
Assume HbUpair.
We prove the intermediate claim HbUB: bU ∈ B.
An exact proof term for the current goal is (andEL (bU ∈ B) (0 ∈ bU ∧ bU ⊆ U) HbUpair).
We prove the intermediate claim HbUrest: 0 ∈ bU ∧ bU ⊆ U.
An exact proof term for the current goal is (andER (bU ∈ B) (0 ∈ bU ∧ bU ⊆ U) HbUpair).
We prove the intermediate claim H0bU: 0 ∈ bU.
An exact proof term for the current goal is (andEL (0 ∈ bU) (bU ⊆ U) HbUrest).
We prove the intermediate claim HbUsub: bU ⊆ U.
An exact proof term for the current goal is (andER (0 ∈ bU) (bU ⊆ U) HbUrest).
Apply (binunionE R_standard_basis R_K_basis bU HbUB) to the current goal.
Assume HbUstd: bU ∈ R_standard_basis.
We prove the intermediate claim Hexa: ∃a ∈ R, bU ∈ {open_interval a b|b ∈ R}.
An exact proof term for the current goal is (famunionE R (λa0 : set ⇒ {open_interval a0 b|b ∈ R}) bU HbUstd).
Apply Hexa to the current goal.
Let a be given.
Assume Hapair.
We prove the intermediate claim HaR: a ∈ R.
An exact proof term for the current goal is (andEL (a ∈ R) (bU ∈ {open_interval a b|b ∈ R}) Hapair).
We prove the intermediate claim HbUfam: bU ∈ {open_interval a b|b ∈ R}.
An exact proof term for the current goal is (andER (a ∈ R) (bU ∈ {open_interval a b|b ∈ R}) Hapair).
We prove the intermediate claim Hexb: ∃b ∈ R, bU = open_interval a b.
An exact proof term for the current goal is (ReplE R (λb0 : set ⇒ open_interval a b0) bU HbUfam).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair.
We prove the intermediate claim HbR: b ∈ R.
An exact proof term for the current goal is (andEL (b ∈ R) (bU = open_interval a b) Hbpair).
We prove the intermediate claim HbUeq: bU = open_interval a b.
An exact proof term for the current goal is (andER (b ∈ R) (bU = open_interval a b) Hbpair).
We prove the intermediate claim H0I: 0 ∈ open_interval a b.
rewrite the current goal using HbUeq (from right to left).
An exact proof term for the current goal is H0bU.
We prove the intermediate claim H0cond: Rlt a 0 ∧ Rlt 0 b.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt a x0 ∧ Rlt x0 b) 0 H0I).
We prove the intermediate claim H0b: Rlt 0 b.
An exact proof term for the current goal is (andER (Rlt a 0) (Rlt 0 b) H0cond).
We prove the intermediate claim HexN: ∃N : set, N ∈ ω ∧ Rlt (inv_nat (ordsucc N)) b.
An exact proof term for the current goal is (exists_inv_nat_ordsucc_lt b HbR H0b).
Apply HexN to the current goal.
Let N be given.
Assume HNpair.
We prove the intermediate claim HNO: N ∈ ω.
An exact proof term for the current goal is (andEL (N ∈ ω) (Rlt (inv_nat (ordsucc N)) b) HNpair).
We prove the intermediate claim Hyltb: Rlt (inv_nat (ordsucc N)) b.
An exact proof term for the current goal is (andER (N ∈ ω) (Rlt (inv_nat (ordsucc N)) b) HNpair).
Set y to be the term inv_nat (ordsucc N).
We prove the intermediate claim HsN: ordsucc N ∈ ω.
An exact proof term for the current goal is (omega_ordsucc N HNO).
We prove the intermediate claim HsNnot0: ordsucc N ∉ {0}.
Assume Hs0: ordsucc N ∈ {0}.
We prove the intermediate claim Heq0: ordsucc N = 0.
An exact proof term for the current goal is (SingE 0 (ordsucc N) Hs0).
An exact proof term for the current goal is ((neq_ordsucc_0 N) Heq0).
We prove the intermediate claim HsNin: ordsucc N ∈ ω ∖ {0}.
An exact proof term for the current goal is (setminusI ω {0} (ordsucc N) HsN HsNnot0).
We prove the intermediate claim HyK: y ∈ K_set.
An exact proof term for the current goal is (ReplI (ω ∖ {0}) (λn0 : set ⇒ inv_nat n0) (ordsucc N) HsNin).
We prove the intermediate claim HyU: y ∈ U.
We prove the intermediate claim HyR: y ∈ R.
An exact proof term for the current goal is (inv_nat_real (ordsucc N) HsN).
We prove the intermediate claim HyPos: Rlt 0 y.
An exact proof term for the current goal is (inv_nat_pos (ordsucc N) HsNin).
We prove the intermediate claim Ha0: Rlt a 0.
An exact proof term for the current goal is (andEL (Rlt a 0) (Rlt 0 b) H0cond).
We prove the intermediate claim Hay: Rlt a y.
An exact proof term for the current goal is (Rlt_tra a 0 y Ha0 HyPos).
We prove the intermediate claim HyI: y ∈ open_interval a b.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt a x0 ∧ Rlt x0 b) y HyR (andI (Rlt a y) (Rlt y b) Hay Hyltb)).
We prove the intermediate claim HybU: y ∈ bU.
rewrite the current goal using HbUeq (from left to right).
An exact proof term for the current goal is HyI.
An exact proof term for the current goal is (HbUsub y HybU).
We prove the intermediate claim HyV: y ∈ V.
An exact proof term for the current goal is (HKsubV y HyK).
We prove the intermediate claim HyUV: y ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V y HyU HyV).
We prove the intermediate claim HyEmpty: y ∈ Empty.
rewrite the current goal using Hdisj (from right to left).
An exact proof term for the current goal is HyUV.
An exact proof term for the current goal is (EmptyE y HyEmpty).
Assume HbUK: bU ∈ R_K_basis.
We prove the intermediate claim Hexa: ∃a ∈ R, bU ∈ {open_interval a b ∖ K_set|b ∈ R}.
An exact proof term for the current goal is (famunionE R (λa0 : set ⇒ {open_interval a0 b ∖ K_set|b ∈ R}) bU HbUK).
Apply Hexa to the current goal.
Let a be given.
Assume Hapair.
We prove the intermediate claim HaR: a ∈ R.
An exact proof term for the current goal is (andEL (a ∈ R) (bU ∈ {open_interval a b ∖ K_set|b ∈ R}) Hapair).
We prove the intermediate claim HbUfam: bU ∈ {open_interval a b ∖ K_set|b ∈ R}.
An exact proof term for the current goal is (andER (a ∈ R) (bU ∈ {open_interval a b ∖ K_set|b ∈ R}) Hapair).
We prove the intermediate claim Hexb: ∃b ∈ R, bU = open_interval a b ∖ K_set.
An exact proof term for the current goal is (ReplE R (λb0 : set ⇒ open_interval a b0 ∖ K_set) bU HbUfam).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair.
We prove the intermediate claim HbR: b ∈ R.
An exact proof term for the current goal is (andEL (b ∈ R) (bU = open_interval a b ∖ K_set) Hbpair).
We prove the intermediate claim HbUeq: bU = open_interval a b ∖ K_set.
An exact proof term for the current goal is (andER (b ∈ R) (bU = open_interval a b ∖ K_set) Hbpair).
We prove the intermediate claim H0bU': 0 ∈ open_interval a b.
We prove the intermediate claim H0bUset: 0 ∈ open_interval a b ∖ K_set.
rewrite the current goal using HbUeq (from right to left).
An exact proof term for the current goal is H0bU.
An exact proof term for the current goal is (setminusE1 (open_interval a b) K_set 0 H0bUset).
We prove the intermediate claim H0cond: Rlt a 0 ∧ Rlt 0 b.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt a x0 ∧ Rlt x0 b) 0 H0bU').
We prove the intermediate claim H0b: Rlt 0 b.
An exact proof term for the current goal is (andER (Rlt a 0) (Rlt 0 b) H0cond).
We prove the intermediate claim HexN: ∃N : set, N ∈ ω ∧ Rlt (inv_nat (ordsucc N)) b.
An exact proof term for the current goal is (exists_inv_nat_ordsucc_lt b HbR H0b).
Apply HexN to the current goal.
Let N be given.
Assume HNpair.
We prove the intermediate claim HNO: N ∈ ω.
An exact proof term for the current goal is (andEL (N ∈ ω) (Rlt (inv_nat (ordsucc N)) b) HNpair).
We prove the intermediate claim Hyltb: Rlt (inv_nat (ordsucc N)) b.
An exact proof term for the current goal is (andER (N ∈ ω) (Rlt (inv_nat (ordsucc N)) b) HNpair).
Set y to be the term inv_nat (ordsucc N).
We prove the intermediate claim HsN: ordsucc N ∈ ω.
An exact proof term for the current goal is (omega_ordsucc N HNO).
We prove the intermediate claim HsNnot0: ordsucc N ∉ {0}.
Assume Hs0: ordsucc N ∈ {0}.
We prove the intermediate claim Heq0: ordsucc N = 0.
An exact proof term for the current goal is (SingE 0 (ordsucc N) Hs0).
An exact proof term for the current goal is ((neq_ordsucc_0 N) Heq0).
We prove the intermediate claim HsNin: ordsucc N ∈ ω ∖ {0}.
An exact proof term for the current goal is (setminusI ω {0} (ordsucc N) HsN HsNnot0).
We prove the intermediate claim HyK: y ∈ K_set.
An exact proof term for the current goal is (ReplI (ω ∖ {0}) (λn0 : set ⇒ inv_nat n0) (ordsucc N) HsNin).
We prove the intermediate claim HyR: y ∈ R.
An exact proof term for the current goal is (inv_nat_real (ordsucc N) HsN).
We prove the intermediate claim HyPos: Rlt 0 y.
An exact proof term for the current goal is (inv_nat_pos (ordsucc N) HsNin).
We prove the intermediate claim Ha0: Rlt a 0.
An exact proof term for the current goal is (andEL (Rlt a 0) (Rlt 0 b) H0cond).
We prove the intermediate claim Hay: Rlt a y.
An exact proof term for the current goal is (Rlt_tra a 0 y Ha0 HyPos).
We prove the intermediate claim Hyab: y ∈ open_interval a b.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt a x0 ∧ Rlt x0 b) y HyR (andI (Rlt a y) (Rlt y b) Hay Hyltb)).
We prove the intermediate claim HyV: y ∈ V.
An exact proof term for the current goal is (HKsubV y HyK).
We prove the intermediate claim HexbV: ∃bV ∈ B, y ∈ bV ∧ bV ⊆ V.
An exact proof term for the current goal is (HVprop y HyV).
Apply HexbV to the current goal.
Let bV be given.
Assume HbVpair.
We prove the intermediate claim HbVB: bV ∈ B.
An exact proof term for the current goal is (andEL (bV ∈ B) (y ∈ bV ∧ bV ⊆ V) HbVpair).
We prove the intermediate claim HbVrest: y ∈ bV ∧ bV ⊆ V.
An exact proof term for the current goal is (andER (bV ∈ B) (y ∈ bV ∧ bV ⊆ V) HbVpair).
We prove the intermediate claim HybV: y ∈ bV.
An exact proof term for the current goal is (andEL (y ∈ bV) (bV ⊆ V) HbVrest).
We prove the intermediate claim HbVsubV: bV ⊆ V.
An exact proof term for the current goal is (andER (y ∈ bV) (bV ⊆ V) HbVrest).
Apply (binunionE R_standard_basis R_K_basis bV HbVB) to the current goal.
Assume HbVstd: bV ∈ R_standard_basis.
We prove the intermediate claim Hexc: ∃c ∈ R, bV ∈ {open_interval c d|d ∈ R}.
An exact proof term for the current goal is (famunionE R (λc0 : set ⇒ {open_interval c0 d|d ∈ R}) bV HbVstd).
Apply Hexc to the current goal.
Let c be given.
Assume Hcpair.
We prove the intermediate claim HcR: c ∈ R.
An exact proof term for the current goal is (andEL (c ∈ R) (bV ∈ {open_interval c d|d ∈ R}) Hcpair).
We prove the intermediate claim HbVfam: bV ∈ {open_interval c d|d ∈ R}.
An exact proof term for the current goal is (andER (c ∈ R) (bV ∈ {open_interval c d|d ∈ R}) Hcpair).
We prove the intermediate claim Hexd: ∃d ∈ R, bV = open_interval c d.
An exact proof term for the current goal is (ReplE R (λd0 : set ⇒ open_interval c d0) bV HbVfam).
Apply Hexd to the current goal.
Let d be given.
Assume Hdpair.
We prove the intermediate claim HdR: d ∈ R.
An exact proof term for the current goal is (andEL (d ∈ R) (bV = open_interval c d) Hdpair).
We prove the intermediate claim HbVeq: bV = open_interval c d.
An exact proof term for the current goal is (andER (d ∈ R) (bV = open_interval c d) Hdpair).
We prove the intermediate claim Hycd: y ∈ open_interval c d.
rewrite the current goal using HbVeq (from right to left).
An exact proof term for the current goal is HybV.
We prove the intermediate claim Hexz: ∃z : set, z ∈ (open_interval a b ∩ open_interval c d) ∧ z ∉ K_set.
An exact proof term for the current goal is (K_set_point_has_nonK_neighbor_in_intersection a b c d y HaR HbR HcR HdR HyK Hyab Hycd).
Apply Hexz to the current goal.
Let z be given.
Assume Hzpair.
We prove the intermediate claim HzI: z ∈ (open_interval a b ∩ open_interval c d).
An exact proof term for the current goal is (andEL (z ∈ (open_interval a b ∩ open_interval c d)) (z ∉ K_set) Hzpair).
We prove the intermediate claim HznotK: z ∉ K_set.
An exact proof term for the current goal is (andER (z ∈ (open_interval a b ∩ open_interval c d)) (z ∉ K_set) Hzpair).
We prove the intermediate claim Hzab: z ∈ open_interval a b.
An exact proof term for the current goal is (binintersectE1 (open_interval a b) (open_interval c d) z HzI).
We prove the intermediate claim Hzcd: z ∈ open_interval c d.
An exact proof term for the current goal is (binintersectE2 (open_interval a b) (open_interval c d) z HzI).
We prove the intermediate claim HzbU: z ∈ bU.
rewrite the current goal using HbUeq (from left to right).
An exact proof term for the current goal is (setminusI (open_interval a b) K_set z Hzab HznotK).
We prove the intermediate claim HzU: z ∈ U.
An exact proof term for the current goal is (HbUsub z HzbU).
We prove the intermediate claim HzbV: z ∈ bV.
rewrite the current goal using HbVeq (from left to right).
An exact proof term for the current goal is Hzcd.
We prove the intermediate claim HzV: z ∈ V.
An exact proof term for the current goal is (HbVsubV z HzbV).
We prove the intermediate claim HzUV: z ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V z HzU HzV).
We prove the intermediate claim HzEmpty: z ∈ Empty.
rewrite the current goal using Hdisj (from right to left).
An exact proof term for the current goal is HzUV.
An exact proof term for the current goal is (EmptyE z HzEmpty).
Assume HbVK: bV ∈ R_K_basis.
We prove the intermediate claim Hexc: ∃c ∈ R, bV ∈ {open_interval c d ∖ K_set|d ∈ R}.
An exact proof term for the current goal is (famunionE R (λc0 : set ⇒ {open_interval c0 d ∖ K_set|d ∈ R}) bV HbVK).
Apply Hexc to the current goal.
Let c be given.
Assume Hcpair.
We prove the intermediate claim HcR: c ∈ R.
An exact proof term for the current goal is (andEL (c ∈ R) (bV ∈ {open_interval c d ∖ K_set|d ∈ R}) Hcpair).
We prove the intermediate claim HbVfam2: bV ∈ {open_interval c d ∖ K_set|d ∈ R}.
An exact proof term for the current goal is (andER (c ∈ R) (bV ∈ {open_interval c d ∖ K_set|d ∈ R}) Hcpair).
We prove the intermediate claim Hexd: ∃d ∈ R, bV = open_interval c d ∖ K_set.
An exact proof term for the current goal is (ReplE R (λd0 : set ⇒ open_interval c d0 ∖ K_set) bV HbVfam2).
Apply Hexd to the current goal.
Let d be given.
Assume Hdpair.
We prove the intermediate claim HbVeq: bV = open_interval c d ∖ K_set.
An exact proof term for the current goal is (andER (d ∈ R) (bV = open_interval c d ∖ K_set) Hdpair).
We prove the intermediate claim HyNotK: y ∉ K_set.
We prove the intermediate claim HybVset: y ∈ open_interval c d ∖ K_set.
rewrite the current goal using HbVeq (from right to left).
An exact proof term for the current goal is HybV.
An exact proof term for the current goal is (setminusE2 (open_interval c d) K_set y HybVset).
An exact proof term for the current goal is (HyNotK HyK).
∎