Let x be given.
Assume HxR: x ∈ R.
Assume H0ltx: 0 < x.
Assume HxnotK: ¬ (x ∈ K_set).
We will prove ∃U : set, U ∈ R_standard_topology ∧ x ∈ U ∧ U ∩ K_set = Empty.
We prove the intermediate claim H0ltxR: Rlt 0 x.
An exact proof term for the current goal is (RltI 0 x real_0 HxR H0ltx).
We prove the intermediate claim Hexb: ∃b : set, b ∈ halfopen_interval_left 0 x ∧ b ∈ K_set.
An exact proof term for the current goal is (K_set_meets_lower_limit_neighborhood_0 0 x real_0 HxR (not_Rlt_refl 0 real_0) H0ltxR).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair.
We prove the intermediate claim Hbhalf: b ∈ halfopen_interval_left 0 x.
An exact proof term for the current goal is (andEL (b ∈ halfopen_interval_left 0 x) (b ∈ K_set) Hbpair).
We prove the intermediate claim HbK: b ∈ K_set.
An exact proof term for the current goal is (andER (b ∈ halfopen_interval_left 0 x) (b ∈ K_set) Hbpair).
We prove the intermediate claim HbR: b ∈ R.
An exact proof term for the current goal is (K_set_Subq_R b HbK).
We prove the intermediate claim Hbprop: ¬ (Rlt b 0) ∧ Rlt b x.
An exact proof term for the current goal is (SepE2 R (λy0 : set ⇒ ¬ (Rlt y0 0) ∧ Rlt y0 x) b Hbhalf).
We prove the intermediate claim HbLtX: Rlt b x.
An exact proof term for the current goal is (andER (¬ (Rlt b 0)) (Rlt b x) Hbprop).
We prove the intermediate claim Hbpos: Rlt 0 b.
Apply (ReplE_impred (ω ∖ {0}) (λn : set ⇒ inv_nat n) b HbK (Rlt 0 b)) to the current goal.
Let n be given.
Assume HnIn: n ∈ ω ∖ {0}.
Assume Hbeq: b = inv_nat n.
rewrite the current goal using Hbeq (from left to right).
An exact proof term for the current goal is (inv_nat_pos n HnIn).
Set V to be the term {y ∈ R|Rlt b y}.
We prove the intermediate claim HVopen: V ∈ R_standard_topology.
An exact proof term for the current goal is (open_ray_in_R_standard_topology b HbR).
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (SepI R (λy0 : set ⇒ Rlt b y0) x HxR HbLtX).
Set F to be the term K_set ∩ V.
We prove the intermediate claim HFfin: finite F.
We prove the intermediate claim HFdef: F = K_set ∩ {y ∈ R|Rlt b y}.
Use reflexivity.
rewrite the current goal using HFdef (from left to right).
An exact proof term for the current goal is (K_set_above_positive_bound_finite b HbR Hbpos).
We prove the intermediate claim HFsubR: F ⊆ R.
Let z be given.
Assume HzF: z ∈ F.
We prove the intermediate claim HzK: z ∈ K_set.
An exact proof term for the current goal is (binintersectE1 K_set V z HzF).
An exact proof term for the current goal is (K_set_Subq_R z HzK).
Set U to be the term V ∩ (R ∖ F).
We prove the intermediate claim HRmF: R ∖ F ∈ R_standard_topology.
An exact proof term for the current goal is (finite_complement_open_in_R_standard_topology F HFfin HFsubR).
We prove the intermediate claim HUopen: U ∈ R_standard_topology.
An exact proof term for the current goal is (topology_binintersect_closed R R_standard_topology V (R ∖ F) (R_standard_topology_is_topology_local) HVopen HRmF).
We prove the intermediate claim HxnotF: x ∉ F.
Assume HxF: x ∈ F.
We prove the intermediate claim HxK': x ∈ K_set.
An exact proof term for the current goal is (binintersectE1 K_set V x HxF).
An exact proof term for the current goal is (HxnotK HxK').
We prove the intermediate claim HxRmF: x ∈ R ∖ F.
An exact proof term for the current goal is (setminusI R F x HxR HxnotF).
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (binintersectI V (R ∖ F) x HxV HxRmF).
We prove the intermediate claim HUempty: U ∩ K_set = Empty.
Apply Empty_Subq_eq to the current goal.
Let z be given.
Assume Hz: z ∈ U ∩ K_set.
We will prove z ∈ Empty.
Apply FalseE to the current goal.
We prove the intermediate claim HzU: z ∈ U.
An exact proof term for the current goal is (binintersectE1 U K_set z Hz).
We prove the intermediate claim HzK: z ∈ K_set.
An exact proof term for the current goal is (binintersectE2 U K_set z Hz).
We prove the intermediate claim HzV_RmF: z ∈ V ∩ (R ∖ F).
An exact proof term for the current goal is HzU.
We prove the intermediate claim HzV: z ∈ V.
An exact proof term for the current goal is (binintersectE1 V (R ∖ F) z HzV_RmF).
We prove the intermediate claim HzRmF: z ∈ R ∖ F.
An exact proof term for the current goal is (binintersectE2 V (R ∖ F) z HzV_RmF).
We prove the intermediate claim HzF: z ∈ F.
An exact proof term for the current goal is (binintersectI K_set V z HzK HzV).
We prove the intermediate claim HznotF: z ∉ F.
An exact proof term for the current goal is (setminusE2 R F z HzRmF).
An exact proof term for the current goal is (HznotF HzF).
We use U to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HUopen.
An exact proof term for the current goal is HxU.
An exact proof term for the current goal is HUempty.
∎