Let X, Tx, A, net, J, le and x be given.
Assume HTx: topology_on X Tx.
Assume HAsub: A ⊆ X.
Assume Hdir: directed_set J le.
Assume HtotA: total_function_on net J A.
Assume Hgraph: functional_graph net.
Assume Hdom: graph_domain_subset net J.
Assume HxA: x ∈ A.
Assume HconvX: net_converges_on X Tx net J le x.
Set TA to be the term subspace_topology X Tx A.
We prove the intermediate claim HTA: topology_on A TA.
An exact proof term for the current goal is (subspace_topology_is_topology X Tx A HTx HAsub).
We will prove net_converges_on A TA net J le x.
We will prove topology_on A TA ∧ directed_set J le ∧ total_function_on net J A ∧ functional_graph net ∧ graph_domain_subset net J ∧ x ∈ A ∧ ∀U : set, U ∈ TA → x ∈ U → ∃i0 : set, i0 ∈ J ∧ ∀i : set, i ∈ J → (i0,i) ∈ le → apply_fun net i ∈ U.
Apply (and7I (topology_on A TA) (directed_set J le) (total_function_on net J A) (functional_graph net) (graph_domain_subset net J) (x ∈ A) (∀U : set, U ∈ TA → x ∈ U → ∃i0 : set, i0 ∈ J ∧ ∀i : set, i ∈ J → (i0,i) ∈ le → apply_fun net i ∈ U)) to the current goal.
An exact proof term for the current goal is HTA.
An exact proof term for the current goal is Hdir.
An exact proof term for the current goal is HtotA.
An exact proof term for the current goal is Hgraph.
An exact proof term for the current goal is Hdom.
An exact proof term for the current goal is HxA.
Let U be given.
Assume HU: U ∈ TA.
Assume HxU: x ∈ U.
Apply (subspace_topologyE X Tx A U HU) to the current goal.
Let V be given.
Assume HVpair.
Apply HVpair to the current goal.
Assume HVTx: V ∈ Tx.
Assume HUEq: U = V ∩ A.
rewrite the current goal using HUEq (from left to right).
We prove the intermediate claim HxV: x ∈ V.
We prove the intermediate claim HxVA: x ∈ V ∩ A.
rewrite the current goal using HUEq (from right to left) at position 1.
An exact proof term for the current goal is HxU.
An exact proof term for the current goal is (binintersectE1 V A x HxVA).
Apply HconvX to the current goal.
Assume Hcore Hevent.
Apply (Hevent V HVTx HxV) to the current goal.
Let i0 be given.
Assume Hi0pair.
We use i0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (andEL (i0 ∈ J) (∀i : set, i ∈ J → (i0,i) ∈ le → apply_fun net i ∈ V) Hi0pair).
Let i be given.
Assume HiJ: i ∈ J.
Assume Hi0i: (i0,i) ∈ le.
We prove the intermediate claim HnetV: apply_fun net i ∈ V.
We prove the intermediate claim HtailV: ∀i1 : set, i1 ∈ J → (i0,i1) ∈ le → apply_fun net i1 ∈ V.
An exact proof term for the current goal is (andER (i0 ∈ J) (∀i1 : set, i1 ∈ J → (i0,i1) ∈ le → apply_fun net i1 ∈ V) Hi0pair).
An exact proof term for the current goal is (HtailV i HiJ Hi0i).
We prove the intermediate claim HnetA: apply_fun net i ∈ A.
An exact proof term for the current goal is (total_function_on_apply_fun_in_Y net J A i HtotA HiJ).
An exact proof term for the current goal is (binintersectI V A (apply_fun net i) HnetV HnetA).
∎