Summary
Sets
If α is some type (α : Type*), then the type of a set s with elements of type α is
s : Set α
The following table summarizes what the types of the proof terms look like for different goals involving sets. To construct proof terms of the correct type, we can use tactics introduced previously.
| Goal | Type of proof term |
|---|---|
| s ⊆ t | ∀ x : α, x ∈ s → x ∈ t |
| x ∈ s ∩ t | x ∈ s ∧ x ∈ t |
| x ∈ s ∪ t | x ∈ s ∨ x ∈ t |
| x ∉ s | x ∈ s → False |
| x ∈ s \ t | x ∈ s ∧ x ∉ t |
Functions
The first exercises focus on images and preimages of functions. Consider the type of the proof terms of the following goals, with the context
α, β : Type*
x : α
y : β
f : α → β
s : Set α
p : Set β
| Goal | Type of proof term |
|---|---|
| y ∈ f '' s | ∃ x, x ∈ s ∧ f x = y |
| x ∈ f ' ⁻¹ p | f x ∈ p |
Next week
…