Commit 5631e485 by Robbert Krebbers

### Cancelation for union.

parent d6875e7d
 ... @@ -339,6 +339,11 @@ Section simple_collection. ... @@ -339,6 +339,11 @@ Section simple_collection. Lemma empty_union X Y : X ∪ Y ≡ ∅ ↔ X ≡ ∅ ∧ Y ≡ ∅. Lemma empty_union X Y : X ∪ Y ≡ ∅ ↔ X ≡ ∅ ∧ Y ≡ ∅. Proof. set_solver. Qed. Proof. set_solver. Qed. Lemma union_cancel_l X Y Z : Z ⊥ X → Z ⊥ Y → Z ∪ X ≡ Z ∪ Y → X ≡ Y. Proof. set_solver. Qed. Lemma union_cancel_r X Y Z : X ⊥ Z → Y ⊥ Z → X ∪ Z ≡ Y ∪ Z → X ≡ Y. Proof. set_solver. Qed. (** Empty *) (** Empty *) Lemma elem_of_equiv_empty X : X ≡ ∅ ↔ ∀ x, x ∉ X. Lemma elem_of_equiv_empty X : X ≡ ∅ ↔ ∀ x, x ∉ X. Proof. set_solver. Qed. Proof. set_solver. Qed. ... @@ -455,6 +460,11 @@ Section simple_collection. ... @@ -455,6 +460,11 @@ Section simple_collection. Lemma empty_union_L X Y : X ∪ Y = ∅ ↔ X = ∅ ∧ Y = ∅. Lemma empty_union_L X Y : X ∪ Y = ∅ ↔ X = ∅ ∧ Y = ∅. Proof. unfold_leibniz. apply empty_union. Qed. Proof. unfold_leibniz. apply empty_union. Qed. Lemma union_cancel_l_L X Y Z : Z ⊥ X → Z ⊥ Y → Z ∪ X = Z ∪ Y → X = Y. Proof. unfold_leibniz. apply union_cancel_l. Qed. Lemma union_cancel_r_L X Y Z : X ⊥ Z → Y ⊥ Z → X ∪ Z = Y ∪ Z → X = Y. Proof. unfold_leibniz. apply union_cancel_r. Qed. (** Empty *) (** Empty *) Lemma elem_of_equiv_empty_L X : X = ∅ ↔ ∀ x, x ∉ X. Lemma elem_of_equiv_empty_L X : X = ∅ ↔ ∀ x, x ∉ X. Proof. unfold_leibniz. apply elem_of_equiv_empty. Qed. Proof. unfold_leibniz. apply elem_of_equiv_empty. Qed. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!