forked from ImperialCollegeLondon/M40001_lean
-
Notifications
You must be signed in to change notification settings - Fork 0
/
sheet6.lean
65 lines (47 loc) · 1.15 KB
/
sheet6.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
/-
Copyright (c) 2021 Kevin Buzzard. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author : Kevin Buzzard
-/
import tactic -- imports all the Lean tactics
/-!
# Sets in Lean, sheet 6 : equality of sets
Sets are extensional objects to mathematicians, which means that
if two sets have the same elements, then they are equal.
## Tactics
Tactics you will need to know for this sheet:
* `ext`
### The `ext` tactic
If the goal is `⊢ A = B` where `A` and `B` are subsets of `X`, then
the tactic `ext x,` will create a hypothesis `x : X` and change
the goal to `x ∈ A ↔ x ∈ B`.
-/
open set
variables
(X : Type) -- Everything will be a subset of `X`
(A B C D E : set X) -- A,B,C,D,E are subsets of `X`
(x y z : X) -- x,y,z are elements of `X` or, more precisely, terms of type `X`
example : A ⊆ B → B ⊆ A → A = B :=
begin
sorry
end
example : A ∪ A = A :=
begin
sorry
end
example : A ∩ A = A :=
begin
sorry
end
example : A ∩ B = B ∩ A :=
begin
sorry
end
example : A ∩ (B ∩ C) = (A ∩ B) ∩ C :=
begin
sorry
end
example : A ∪ (B ∪ C) = (A ∪ B) ∪ C :=
begin
sorry
end