Skip to content
Snippets Groups Projects
Commit e37b4e68 authored by Ralf Jung's avatar Ralf Jung
Browse files

add set_map_empty

parent bf59b1eb
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 4 additions and 0 deletions
theories/fin_sets.v
+ 4
− 0
View file @ e37b4e68
...@@ -343,6 +343,10 @@ Section map. ...@@ -343,6 +343,10 @@ Section map.
x ∈ X → y = f x → y ∈ set_map (D:=D) f X. x ∈ X → y = f x → y ∈ set_map (D:=D) f X.
Proof. set_solver. Qed. Proof. set_solver. Qed.
Lemma set_map_empty (f : A → B) :
set_map (C:=C) (D:=D) f ∅ = ∅.
Proof. unfold set_map. rewrite elements_empty. done. Qed.
Lemma set_map_union (f : A → B) (X Y : C) : Lemma set_map_union (f : A → B) (X Y : C) :
set_map (D:=D) f (X ∪ Y) ≡ set_map (D:=D) f X ∪ set_map (D:=D) f Y. set_map (D:=D) f (X ∪ Y) ≡ set_map (D:=D) f X ∪ set_map (D:=D) f Y.
Proof. set_solver. Qed. Proof. set_solver. Qed.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment