definition discrete_uniform_space_of_bishop_set:bishop_set → uniform_space.
intro C; apply (mk_uniform_space C);
[1: intro; apply (∃_:unit.∀n:C square.(fst n ≈ snd n → P n) ∧ (P n → fst n ≈ snd n));
definition discrete_uniform_space_of_bishop_set:bishop_set → uniform_space.
intro C; apply (mk_uniform_space C);
[1: intro; apply (∃_:unit.∀n:C square.(fst n ≈ snd n → P n) ∧ (P n → fst n ≈ snd n));
cases H (_ H1); cases (H1 x); apply H2; apply Hx;
|3: intros; cases H (_ PU); cases H1 (_ PV);
exists[apply (λx.U x ∧ V x)] split;
[1: exists[apply something] intro; cases (PU n); cases (PV n);
split; intros; try split;[apply H2;|apply H4] try assumption;
apply H3; cases H6; assumption;
cases H (_ H1); cases (H1 x); apply H2; apply Hx;
|3: intros; cases H (_ PU); cases H1 (_ PV);
exists[apply (λx.U x ∧ V x)] split;
[1: exists[apply something] intro; cases (PU n); cases (PV n);
split; intros; try split;[apply H2;|apply H4] try assumption;
apply H3; cases H6; assumption;
|4: intros; cases H (_ PU); exists [apply U] split;
[1: exists [apply something] intro n; cases (PU n);
split; intros; try split;[apply H1;|apply H2] assumption;
|4: intros; cases H (_ PU); exists [apply U] split;
[1: exists [apply something] intro n; cases (PU n);
split; intros; try split;[apply H1;|apply H2] assumption;
lemma nat_dedekind_sigma_complete:
∀l,u:ℕ.∀a:sequence {[l,u]}.a is_increasing →
∀x.x is_supremum a → ∃i.∀j.i ≤ j → fst x = fst (a j).
lemma nat_dedekind_sigma_complete:
∀l,u:ℕ.∀a:sequence {[l,u]}.a is_increasing →
∀x.x is_supremum a → ∃i.∀j.i ≤ j → fst x = fst (a j).
apply os_le_to_nat_le; lapply (nat_le_to_os_le ?? H7) as H77;
apply(trans_increasing ?? H (S n2) (pred) H77);]]]]]
clearbody m; unfold spec in m; clear spec;
apply os_le_to_nat_le; lapply (nat_le_to_os_le ?? H7) as H77;
apply(trans_increasing ?? H (S n2) (pred) H77);]]]]]
clearbody m; unfold spec in m; clear spec;