Issue creating simple topological space #32
Comments
|
According to the definition the reduced goal is: So we just need a classical choice on whether a, b, and c are in the set: Thus you gain 8 subgoals, each of them is pretty straightforward. |
|
Thanks, that helps but I have the following goal which seems impossible: |
|
As any topology, From Coq Require Import Ensembles.
From ZornsLemma Require Import EnsemblesTactics.
From Topology Require Import TopologicalSpaces.
Section TopSpaceEx1.
Inductive X : Type := a | b | c.
Definition T (x : Ensemble X) : Prop := Same_set x Empty_set
\/ Same_set x (Singleton b)
\/ Same_set x (Couple b c)
\/ Same_set x (Couple a b)
\/ Same_set x Full_set.
Ltac split_destruct_x :=
split; red; intros x ?; destruct x.
Ltac destruct_or :=
repeat match goal with
| [H: _ \/ _ |- _] => destruct H as [H | H]
| [H: Same_set _ _ |- _] => apply Extensionality_Ensembles in H
end; subst.
Ltac firstorder_or tac :=
match goal with
| [ |- _ \/ _] => try (left; firstorder_or tac); try (right; firstorder_or tac)
| _ => tac; fail
end.
Lemma T_is_topology : TopologicalSpace.
Proof.
refine (Build_TopologicalSpace X T _ _ ltac:(firstorder));
intros; unfold T in *.
- destruct (classic (In (FamilyUnion F) a)),
(classic (In (FamilyUnion F) b)),
(classic (In (FamilyUnion F) c));
firstorder_or ltac:(split_destruct_x; easy + constructor);
match goal with
| [HH: In _ _ |- _] => inversion HH
end;
pose proof (H _ H3);
destruct_or;
easy + contradict H1;
repeat (econstructor + eassumption).
- destruct_or;
firstorder_or ltac:(now repeat (split_destruct_x; inversion_ensembles_in) + constructor).
Qed.
End TopSpaceEx1. |
|
Ah, interesting. I assumed that adding the empty set would be redundant because this was already proven in Lemma open_empty: forall X:TopologicalSpace, open (@Empty_set X). |
|
From Coq Require Import Ensembles.
From ZornsLemma Require Import EnsemblesTactics.
From Topology Require Import TopologicalSpaces OpenBases.
Section TopSpaceEx1.
Inductive X : Type := a | b | c.
Ltac destruct_or :=
repeat match goal with
| [H: _ \/ _ |- _] => destruct H as [H | H]
| [H: Same_set _ _ |- _] => apply Extensionality_Ensembles in H
end; subst.
Definition B (x : Ensemble X) : Prop := Same_set x (Singleton b)
\/ Same_set x (Couple b c)
\/ Same_set x (Couple a b).
Lemma B_couple_a : forall W, In W a -> In B W -> W = (Couple a b).
Proof.
intros.
extensionality_ensembles_inv;
destruct_or;
try apply Extensionality_Ensembles in H2;
subst;
try destruct H1;
easy + right.
Qed.
Lemma B_couple_c : forall W, In W c -> In B W -> W = (Couple b c).
Proof.
intros.
extensionality_ensembles_inv;
destruct_or;
try apply Extensionality_Ensembles in H2;
subst;
try destruct H1;
easy + left.
Qed.
Lemma B_is_basis : TopologicalSpace.
Proof.
refine (Build_TopologicalSpace_from_open_basis B _ _);
red; intros;
try destruct H1;
destruct x.
- rewrite (B_couple_a _ H1 H), (B_couple_a _ H2 H0).
exists (Couple a b).
repeat split; trivial + (do 3 constructor);
now red; intros.
- exists (Singleton b).
repeat split;
try now destruct H3.
left.
now split; red; intros.
- rewrite (B_couple_c _ H1 H), (B_couple_c _ H2 H0).
exists (Couple b c).
repeat split; trivial + (do 3 constructor);
now red; intros.
- exists (Couple a b).
now repeat (right + constructor).
- exists (Singleton b).
now repeat constructor.
- exists (Couple b c).
now repeat (right + constructor).
Qed.
End TopSpaceEx1. |
|
Constructing the topological space from a subbasis should be even easier, because subbases don't have to satisfy any conditions. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
I want to create a very simple topological space on
X={a,b,c}with the open setsT={{b},{b,c},{a,b},X,∅}, but I'm having great difficulty in doing so (code below). In particular, I'm stuck on this goal (see the location ofadmitin the code):also, is there a way to perform reflection on Ensembles to discharge the easy proof about being closed under finite intersections?
The text was updated successfully, but these errors were encountered: