Let X, Tx, net and x be given.
Assume Hconv: net_converges X Tx net x.
We will prove accumulation_point_of_net X Tx net x.
Apply Hconv to the current goal.
Let J be given.
Assume HJ: ∃le : set, topology_on X Tx ∧ directed_set J le ∧ total_function_on net J X ∧ functional_graph net ∧ graph_domain_subset net J ∧ x ∈ X ∧ ∀U : set, U ∈ Tx → x ∈ U → ∃i0 : set, i0 ∈ J ∧ ∀i : set, i ∈ J → (i0,i) ∈ le → apply_fun net i ∈ U.
Apply HJ to the current goal.
Let le be given.
Assume Hdata: topology_on X Tx ∧ directed_set J le ∧ total_function_on net J X ∧ functional_graph net ∧ graph_domain_subset net J ∧ x ∈ X ∧ ∀U : set, U ∈ Tx → x ∈ U → ∃i0 : set, i0 ∈ J ∧ ∀i : set, i ∈ J → (i0,i) ∈ le → apply_fun net i ∈ U.
We will prove accumulation_point_of_net X Tx net x.
We will prove ∃J0 le0 : set, topology_on X Tx ∧ directed_set J0 le0 ∧ total_function_on net J0 X ∧ functional_graph net ∧ graph_domain_subset net J0 ∧ x ∈ X ∧ ∀U : set, U ∈ Tx → x ∈ U → ∀j0 : set, j0 ∈ J0 → ∃j : set, j ∈ J0 ∧ (j0,j) ∈ le0 ∧ apply_fun net j ∈ U.
We use J to witness the existential quantifier.
We use le to witness the existential quantifier.
Apply Hdata to the current goal.
Assume Hcore Hevent.
Apply Hcore to the current goal.
Assume Hcore5 HxX.
Apply Hcore5 to the current goal.
Assume Hcore4 Hdom.
Apply Hcore4 to the current goal.
Assume Hcore3 Hgraph.
Apply Hcore3 to the current goal.
Assume Hcore2 Htot.
Apply Hcore2 to the current goal.
Assume HTx HdirJ.
Apply andI to the current goal.
We will prove topology_on X Tx ∧ directed_set J le ∧ total_function_on net J X ∧ functional_graph net ∧ graph_domain_subset net J ∧ x ∈ X.
Apply and6I to the current goal.
An exact proof term for the current goal is HTx.
An exact proof term for the current goal is HdirJ.
An exact proof term for the current goal is Htot.
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 HxX.
Let U be given.
Assume HU: U ∈ Tx.
Assume HxU: x ∈ U.
Let j0 be given.
Assume Hj0J: j0 ∈ J.
We will prove ∃j : set, j ∈ J ∧ (j0,j) ∈ le ∧ apply_fun net j ∈ U.
We prove the intermediate claim Hexi0: ∃i0 : set, i0 ∈ J ∧ ∀i : set, i ∈ J → (i0,i) ∈ le → apply_fun net i ∈ U.
An exact proof term for the current goal is (Hevent U HU HxU).
Apply Hexi0 to the current goal.
Let i0 be given.
Assume Hi0pair.
Apply Hi0pair to the current goal.
Assume Hi0J Hafter.
We prove the intermediate claim Hexk: ∃k : set, k ∈ J ∧ (j0,k) ∈ le ∧ (i0,k) ∈ le.
An exact proof term for the current goal is (directed_set_upper_bound_property J le HdirJ j0 i0 Hj0J Hi0J).
Apply Hexk to the current goal.
Let k be given.
Assume Hk.
Apply Hk to the current goal.
Assume Hkleft Hik.
Apply Hkleft to the current goal.
Assume HkJ Hjk.
We use k to witness the existential quantifier.
Apply and3I to the current goal.
An exact proof term for the current goal is HkJ.
An exact proof term for the current goal is Hjk.
An exact proof term for the current goal is (Hafter k HkJ Hik).
∎