Let Fam be given.
Assume Hcount: countable_set Fam.
Assume Hclosed: ∀C : set, C ∈ Fam → closed_in R R_standard_topology C ∧ (∀U : set, U ∈ R_standard_topology → U ⊆ C → U = Empty).
We will prove R ≠ ⋃ Fam.
Assume Heq: R = ⋃ Fam.
We will prove False.
We prove the intermediate claim HBc_metric: Baire_space_closed R (metric_topology R R_bounded_metric).
An exact proof term for the current goal is (Baire_category_complete_metric_closed R R_bounded_metric R_bounded_metric_complete).
We prove the intermediate claim HBc: Baire_space_closed R R_standard_topology.
rewrite the current goal using metric_topology_R_bounded_metric_eq_R_standard_topology (from right to left).
An exact proof term for the current goal is HBc_metric.
We prove the intermediate claim HT: topology_on R R_standard_topology.
An exact proof term for the current goal is (andEL (topology_on R R_standard_topology) (∀Fam0 : set, countable_set Fam0 → (∀A : set, A ∈ Fam0 → closed_in R R_standard_topology A ∧ interior_of R R_standard_topology A = Empty) → interior_of R R_standard_topology (⋃ Fam0) = Empty) HBc).
We prove the intermediate claim HBc_prop: ∀Fam0 : set, countable_set Fam0 → (∀A : set, A ∈ Fam0 → closed_in R R_standard_topology A ∧ interior_of R R_standard_topology A = Empty) → interior_of R R_standard_topology (⋃ Fam0) = Empty.
An exact proof term for the current goal is (andER (topology_on R R_standard_topology) (∀Fam0 : set, countable_set Fam0 → (∀A : set, A ∈ Fam0 → closed_in R R_standard_topology A ∧ interior_of R R_standard_topology A = Empty) → interior_of R R_standard_topology (⋃ Fam0) = Empty) HBc).
We prove the intermediate claim HFam_prop: ∀C : set, C ∈ Fam → closed_in R R_standard_topology C ∧ interior_of R R_standard_topology C = Empty.
Let C be given.
Assume HC: C ∈ Fam.
We prove the intermediate claim Hpack: closed_in R R_standard_topology C ∧ (∀U : set, U ∈ R_standard_topology → U ⊆ C → U = Empty).
An exact proof term for the current goal is (Hclosed C HC).
We prove the intermediate claim Hcl: closed_in R R_standard_topology C.
An exact proof term for the current goal is (andEL (closed_in R R_standard_topology C) (∀U : set, U ∈ R_standard_topology → U ⊆ C → U = Empty) Hpack).
We prove the intermediate claim Hnoopen: ∀U : set, U ∈ R_standard_topology → U ⊆ C → U = Empty.
An exact proof term for the current goal is (andER (closed_in R R_standard_topology C) (∀U : set, U ∈ R_standard_topology → U ⊆ C → U = Empty) Hpack).
We prove the intermediate claim Hint: interior_of R R_standard_topology C = Empty.
Apply (Hnoopen (interior_of R R_standard_topology C)) to the current goal.
We prove the intermediate claim HCsubR: C ⊆ R.
An exact proof term for the current goal is (closed_in_subset R R_standard_topology C Hcl).
An exact proof term for the current goal is (interior_is_open R R_standard_topology C HT HCsubR).
An exact proof term for the current goal is (interior_subset R R_standard_topology C HT).
Apply andI to the current goal.
An exact proof term for the current goal is Hcl.
An exact proof term for the current goal is Hint.
We prove the intermediate claim HintUnion: interior_of R R_standard_topology (⋃ Fam) = Empty.
An exact proof term for the current goal is (HBc_prop Fam Hcount HFam_prop).
We prove the intermediate claim HintR: interior_of R R_standard_topology R = R.
An exact proof term for the current goal is (interior_of_space R R_standard_topology HT).
We prove the intermediate claim HintR_empty: interior_of R R_standard_topology R = Empty.
rewrite the current goal using Heq (from left to right) at position 2.
An exact proof term for the current goal is HintUnion.
We prove the intermediate claim HRE: R = Empty.
rewrite the current goal using HintR (from right to left).
An exact proof term for the current goal is HintR_empty.
We prove the intermediate claim HRne: R ≠ Empty.
An exact proof term for the current goal is (elem_implies_nonempty R 0 real_0).
An exact proof term for the current goal is (HRne HRE).
∎