We will prove discrete_subspace real_sequences uniform_topology binary_sequences_Romega.
We will prove binary_sequences_Romega ⊆ real_sequences ∧ (∀a : set, a ∈ binary_sequences_Romega → ∃U : set, U ∈ uniform_topology ∧ U ∩ binary_sequences_Romega = {a}).
Apply andI to the current goal.
Let f be given.
Assume Hf: f ∈ binary_sequences_Romega.
We will prove f ∈ real_sequences.
An exact proof term for the current goal is (SepE1 real_sequences (λf0 : set ⇒ ∀n : set, n ∈ ω → apply_fun f0 n ∈ {0,1}) f Hf).
Let a be given.
Assume Ha: a ∈ binary_sequences_Romega.
Set U to be the term open_ball real_sequences uniform_metric_Romega a 1.
We use U to witness the existential quantifier.
We will prove U ∈ uniform_topology ∧ U ∩ binary_sequences_Romega = {a}.
Apply andI to the current goal.
We prove the intermediate claim HaX: a ∈ real_sequences.
An exact proof term for the current goal is (SepE1 real_sequences (λf0 : set ⇒ ∀n : set, n ∈ ω → apply_fun f0 n ∈ {0,1}) a Ha).
We prove the intermediate claim H0lt1: Rlt 0 1.
An exact proof term for the current goal is Rlt_0_1.
An exact proof term for the current goal is (open_ball_in_metric_topology real_sequences uniform_metric_Romega a 1 uniform_metric_Romega_is_metric HaX H0lt1).
Apply set_ext to the current goal.
Let f be given.
Assume HfUA: f ∈ U ∩ binary_sequences_Romega.
We will prove f ∈ {a}.
We prove the intermediate claim HfU: f ∈ U.
An exact proof term for the current goal is (binintersectE1 U binary_sequences_Romega f HfUA).
We prove the intermediate claim HfA: f ∈ binary_sequences_Romega.
An exact proof term for the current goal is (binintersectE2 U binary_sequences_Romega f HfUA).
We prove the intermediate claim Hdistlt: Rlt (apply_fun uniform_metric_Romega (a,f)) 1.
An exact proof term for the current goal is (open_ballE2 real_sequences uniform_metric_Romega a 1 f HfU).
Apply (xm (f = a) (f ∈ {a})) to the current goal.
Assume Hfa: f = a.
rewrite the current goal using Hfa (from left to right).
An exact proof term for the current goal is (SingI a).
Assume Hfna: ¬ (f = a).
We prove the intermediate claim Hdist1: apply_fun uniform_metric_Romega (a,f) = 1.
Apply (uniform_metric_Romega_binary_dist_1 a f Ha HfA) to the current goal.
Assume Heq: a = f.
Apply Hfna to the current goal.
Use symmetry.
An exact proof term for the current goal is Heq.
We prove the intermediate claim Hbad: Rlt 1 1.
rewrite the current goal using Hdist1 (from right to left) at position 1.
An exact proof term for the current goal is Hdistlt.
An exact proof term for the current goal is (FalseE ((not_Rlt_refl 1 real_1) Hbad) (f ∈ {a})).
Let f be given.
Assume Hf: f ∈ {a}.
We will prove f ∈ U ∩ binary_sequences_Romega.
We prove the intermediate claim Hfa: f = a.
An exact proof term for the current goal is (singleton_elem f a Hf).
rewrite the current goal using Hfa (from left to right).
Apply (binintersectI U binary_sequences_Romega a) to the current goal.
We prove the intermediate claim HaX: a ∈ real_sequences.
An exact proof term for the current goal is (SepE1 real_sequences (λf0 : set ⇒ ∀n : set, n ∈ ω → apply_fun f0 n ∈ {0,1}) a Ha).
We prove the intermediate claim H0lt1: Rlt 0 1.
An exact proof term for the current goal is Rlt_0_1.
An exact proof term for the current goal is (center_in_open_ball real_sequences uniform_metric_Romega a 1 uniform_metric_Romega_is_metric HaX H0lt1).
An exact proof term for the current goal is Ha.
∎