We will prove bounded_sequences_Romega ∪ unbounded_sequences_Romega = R_omega_space.
Apply set_ext to the current goal.
Let f be given.
Assume Hf: f ∈ bounded_sequences_Romega ∪ unbounded_sequences_Romega.
We will prove f ∈ R_omega_space.
Apply (binunionE bounded_sequences_Romega unbounded_sequences_Romega f Hf) to the current goal.
Assume Hb: f ∈ bounded_sequences_Romega.
An exact proof term for the current goal is (SepE1 R_omega_space (λf0 : set ⇒ bounded_sequence_Romega f0) f Hb).
Assume Hu: f ∈ unbounded_sequences_Romega.
An exact proof term for the current goal is (SepE1 R_omega_space (λf0 : set ⇒ unbounded_sequence_Romega f0) f Hu).
Let f be given.
Assume Hf: f ∈ R_omega_space.
We will prove f ∈ bounded_sequences_Romega ∪ unbounded_sequences_Romega.
Apply (xm (bounded_sequence_Romega f) (f ∈ bounded_sequences_Romega ∪ unbounded_sequences_Romega)) to the current goal.
Assume Hbseq: bounded_sequence_Romega f.
We will prove f ∈ bounded_sequences_Romega ∪ unbounded_sequences_Romega.
Apply binunionI1 to the current goal.
An exact proof term for the current goal is (SepI R_omega_space (λf0 : set ⇒ bounded_sequence_Romega f0) f Hf Hbseq).
Assume HnotBound: ¬ (bounded_sequence_Romega f).
We will prove f ∈ bounded_sequences_Romega ∪ unbounded_sequences_Romega.
Apply binunionI2 to the current goal.
We will prove f ∈ unbounded_sequences_Romega.
Apply (SepI R_omega_space (λf0 : set ⇒ unbounded_sequence_Romega f0) f Hf) to the current goal.
We will prove unbounded_sequence_Romega f.
Let M be given.
Assume HM: M ∈ R.
Apply (xm (∃n : set, n ∈ ω ∧ ¬ (apply_fun f n ∈ open_interval (minus_SNo M) M))) to the current goal.
Assume Hex.
An exact proof term for the current goal is Hex.
Assume Hnone: ¬ (∃n : set, n ∈ ω ∧ ¬ (apply_fun f n ∈ open_interval (minus_SNo M) M)).
We will prove ∃n : set, n ∈ ω ∧ ¬ (apply_fun f n ∈ open_interval (minus_SNo M) M).
Apply FalseE to the current goal.
We will prove False.
Apply HnotBound to the current goal.
We will prove bounded_sequence_Romega f.
We prove the intermediate claim HbndM: ∀n : set, n ∈ ω → apply_fun f n ∈ open_interval (minus_SNo M) M.
Let n be given.
Assume HnO: n ∈ ω.
We will prove apply_fun f n ∈ open_interval (minus_SNo M) M.
Apply dneg to the current goal.
Assume Hnnot: ¬ (apply_fun f n ∈ open_interval (minus_SNo M) M).
We will prove False.
Apply Hnone to the current goal.
We use n to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HnO.
An exact proof term for the current goal is Hnnot.
An exact proof term for the current goal is (λP Hp ⇒ Hp M (andI (M ∈ R) (∀n : set, n ∈ ω → apply_fun f n ∈ open_interval (minus_SNo M) M) HM HbndM)).
∎