Let X, d and seq be given.
Assume H.
We prove the intermediate claim Hleft: metric_on_total X d ∧ sequence_on seq X.
An exact proof term for the current goal is (andEL (metric_on_total X d ∧ sequence_on seq X) (∀eps : set, eps ∈ R ∧ Rlt 0 eps → ∃N : set, N ∈ ω ∧ ∀m n : set, m ∈ ω → n ∈ ω → N ⊆ m → N ⊆ n → Rlt (apply_fun d (apply_fun seq m,apply_fun seq n)) eps) H).
We prove the intermediate claim Hmt: metric_on_total X d.
An exact proof term for the current goal is (andEL (metric_on_total X d) (sequence_on seq X) Hleft).
We prove the intermediate claim Hseq: sequence_on seq X.
An exact proof term for the current goal is (andER (metric_on_total X d) (sequence_on seq X) Hleft).
We prove the intermediate claim Htail: ∀eps : set, eps ∈ R ∧ Rlt 0 eps → ∃N : set, N ∈ ω ∧ ∀m n : set, m ∈ ω → n ∈ ω → N ⊆ m → N ⊆ n → Rlt (apply_fun d (apply_fun seq m,apply_fun seq n)) eps.
An exact proof term for the current goal is (andER (metric_on_total X d ∧ sequence_on seq X) (∀eps : set, eps ∈ R ∧ Rlt 0 eps → ∃N : set, N ∈ ω ∧ ∀m n : set, m ∈ ω → n ∈ ω → N ⊆ m → N ⊆ n → Rlt (apply_fun d (apply_fun seq m,apply_fun seq n)) eps) H).
We will prove metric_on X d ∧ sequence_on seq X ∧ ∀eps : set, eps ∈ R ∧ Rlt 0 eps → ∃N : set, N ∈ ω ∧ ∀m n : set, m ∈ ω → n ∈ ω → N ⊆ m → N ⊆ n → Rlt (apply_fun d (apply_fun seq m,apply_fun seq n)) eps.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (metric_on_total_imp_metric_on X d Hmt).
An exact proof term for the current goal is Hseq.
An exact proof term for the current goal is Htail.
∎