Let a, b and c be given.
Assume HaR: a ∈ R.
Assume HbR: b ∈ R.
Assume HcR: c ∈ R.
Assume Hbne: b ≠ 0.
Assume Hsign: same_sign_nonzero_R a b.
Set g to be the term projection1 R R.
We will prove continuous_map (affine_line_R2 a b c) (subspace_topology (setprod R R) (product_topology R R_lower_limit_topology R R_lower_limit_topology) (affine_line_R2 a b c)) R (discrete_topology R) g.
We prove the intermediate claim HTll: topology_on R R_lower_limit_topology.
An exact proof term for the current goal is R_lower_limit_topology_is_topology.
We prove the intermediate claim HTprod: topology_on (setprod R R) (product_topology R R_lower_limit_topology R R_lower_limit_topology).
An exact proof term for the current goal is (product_topology_is_topology R R_lower_limit_topology R R_lower_limit_topology HTll HTll).
We prove the intermediate claim HLsub: affine_line_R2 a b c ⊆ setprod R R.
An exact proof term for the current goal is (affine_line_R2_subset_R2 a b c).
We prove the intermediate claim HTL: topology_on (affine_line_R2 a b c) (subspace_topology (setprod R R) (product_topology R R_lower_limit_topology R R_lower_limit_topology) (affine_line_R2 a b c)).
An exact proof term for the current goal is (subspace_topology_is_topology (setprod R R) (product_topology R R_lower_limit_topology R R_lower_limit_topology) (affine_line_R2 a b c) HTprod HLsub).
We prove the intermediate claim HTd: topology_on R (discrete_topology R).
An exact proof term for the current goal is (discrete_topology_on R).
We prove the intermediate claim Hfun: function_on g (affine_line_R2 a b c) R.
Let p be given.
Assume HpL: p ∈ affine_line_R2 a b c.
We will prove apply_fun g p ∈ R.
We prove the intermediate claim HpRR: p ∈ setprod R R.
An exact proof term for the current goal is (HLsub p HpL).
We prove the intermediate claim Happ: apply_fun g p = p 0.
An exact proof term for the current goal is (projection1_apply R R p HpRR).
rewrite the current goal using Happ (from left to right).
An exact proof term for the current goal is (ap0_Sigma R (λ_ : set ⇒ R) p HpRR).
We will prove topology_on (affine_line_R2 a b c) (subspace_topology (setprod R R) (product_topology R R_lower_limit_topology R R_lower_limit_topology) (affine_line_R2 a b c)) ∧ topology_on R (discrete_topology R) ∧ function_on g (affine_line_R2 a b c) R ∧ ∀V : set, V ∈ discrete_topology R → preimage_of (affine_line_R2 a b c) g V ∈ (subspace_topology (setprod R R) (product_topology R R_lower_limit_topology R R_lower_limit_topology) (affine_line_R2 a b c)).
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HTL.
An exact proof term for the current goal is HTd.
An exact proof term for the current goal is Hfun.
Let V be given.
Assume HV: V ∈ discrete_topology R.
We will prove preimage_of (affine_line_R2 a b c) g V ∈ (subspace_topology (setprod R R) (product_topology R R_lower_limit_topology R R_lower_limit_topology) (affine_line_R2 a b c)).
Set S to be the term preimage_of (affine_line_R2 a b c) g V.
Set Fam to be the term {{p0}|p0 ∈ S}.
We prove the intermediate claim HFamSub: Fam ⊆ (subspace_topology (setprod R R) (product_topology R R_lower_limit_topology R R_lower_limit_topology) (affine_line_R2 a b c)).
Let U be given.
Assume HU: U ∈ Fam.
We will prove U ∈ (subspace_topology (setprod R R) (product_topology R R_lower_limit_topology R R_lower_limit_topology) (affine_line_R2 a b c)).
We prove the intermediate claim Hex: ∃p0 ∈ S, U = {p0}.
An exact proof term for the current goal is (ReplE S (λp0 : set ⇒ {p0}) U HU).
Apply Hex to the current goal.
Let p0 be given.
Assume Hp0pair.
We prove the intermediate claim Hp0S: p0 ∈ S.
An exact proof term for the current goal is (andEL (p0 ∈ S) (U = {p0}) Hp0pair).
We prove the intermediate claim HUeq: U = {p0}.
An exact proof term for the current goal is (andER (p0 ∈ S) (U = {p0}) Hp0pair).
rewrite the current goal using HUeq (from left to right).
We prove the intermediate claim Hp0L: p0 ∈ affine_line_R2 a b c.
An exact proof term for the current goal is (SepE1 (affine_line_R2 a b c) (λu : set ⇒ apply_fun g u ∈ V) p0 Hp0S).
An exact proof term for the current goal is (affine_line_R2_singleton_open_same_sign a b c p0 HaR HbR HcR Hbne Hsign Hp0L).
We prove the intermediate claim HUnionOpen: ⋃ Fam ∈ (subspace_topology (setprod R R) (product_topology R R_lower_limit_topology R R_lower_limit_topology) (affine_line_R2 a b c)).
An exact proof term for the current goal is (topology_union_closed (affine_line_R2 a b c) (subspace_topology (setprod R R) (product_topology R R_lower_limit_topology R R_lower_limit_topology) (affine_line_R2 a b c)) Fam HTL HFamSub).
We prove the intermediate claim HUnionEq: ⋃ Fam = S.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ ⋃ Fam.
We will prove x ∈ S.
We prove the intermediate claim HexU: ∃U : set, x ∈ U ∧ U ∈ Fam.
An exact proof term for the current goal is (UnionE Fam x Hx).
Apply HexU to the current goal.
Let U be given.
Assume HUconj.
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (andEL (x ∈ U) (U ∈ Fam) HUconj).
We prove the intermediate claim HUfam: U ∈ Fam.
An exact proof term for the current goal is (andER (x ∈ U) (U ∈ Fam) HUconj).
We prove the intermediate claim Hex: ∃p0 ∈ S, U = {p0}.
An exact proof term for the current goal is (ReplE S (λp0 : set ⇒ {p0}) U HUfam).
Apply Hex to the current goal.
Let p0 be given.
Assume Hp0pair.
We prove the intermediate claim Hp0S: p0 ∈ S.
An exact proof term for the current goal is (andEL (p0 ∈ S) (U = {p0}) Hp0pair).
We prove the intermediate claim HUeq: U = {p0}.
An exact proof term for the current goal is (andER (p0 ∈ S) (U = {p0}) Hp0pair).
We prove the intermediate claim HxU2: x ∈ {p0}.
rewrite the current goal using HUeq (from right to left).
An exact proof term for the current goal is HxU.
We prove the intermediate claim Hxeq: x = p0.
An exact proof term for the current goal is (SingE p0 x HxU2).
rewrite the current goal using Hxeq (from left to right).
An exact proof term for the current goal is Hp0S.
Let x be given.
Assume Hx: x ∈ S.
We will prove x ∈ ⋃ Fam.
We prove the intermediate claim HsingFam: {x} ∈ Fam.
An exact proof term for the current goal is (ReplI S (λp0 : set ⇒ {p0}) x Hx).
An exact proof term for the current goal is (UnionI Fam x {x} (SingI x) HsingFam).
rewrite the current goal using HUnionEq (from right to left).
An exact proof term for the current goal is HUnionOpen.
∎