Skip to content

Instantly share code, notes, and snippets.

@matthew-piziak

matthew-piziak/Munkres.v

Created May 4, 2019 22:15
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save matthew-piziak/7d2f1bf53260147a7826072a97658238 to your computer and use it in GitHub Desktop.
Save matthew-piziak/7d2f1bf53260147a7826072a97658238 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
Munkres.v
Theorem exercise_1_2_1: forall A B C : Ensemble U,
Included U A B /\ Included U A C <-> Included U A (Intersection U B C).
Proof.
intros.
split.
intros.
destruct H.
apply Intersection_maximal; assumption.
intros.
split.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment