Functions
2.2.1 Function Composition
Definition
Given two functions $f : A → B$, $g : B → C$ where $A, B, C$ are sets, then $(g ∘ f)(x)$ (the composition of $g$ and $f$) is $g(f(x))$.
def my_composition {A B C : Type u} (f : A → B) (g : B → C) := λ x : A, g (f x)
Remark. Here, to define $\tt{my_composition}$ we used something called lambda abstraction $\tt{λ x : A, g (f x)}$. This is essentially saying we are mapping $\tt{x}$ with type $\tt{A}$ to $\tt{g(f(x))}$. Read more about lambda abstraction here or here.
2.3 Injectivity, Surjectivity and Bijectivity
Definition
A function $f : X → Y$ is called injective if distinct elements of $X$ get mapped to distinct elements of $Y$. More formally, $f$ is injective if $∀ a, b ∈ X, f(a) = f(b) ⇒ a = b$.
def my_injective {X Y : Type u} (f : X → Y) := ∀ a b : X, f(a) = f(b) → a = b
Definition
A function $f : X → Y$ is called surjective if every element of $Y$ gets "hit" by $f$. More formally, $f$ is surjective if $∀ y ∈ Y, ∃ x ∈ X$ such that $f(x) = y$.
def my_surjective {X Y : Type u} (f : X → Y) := ∀ y : Y, ∃ x : X, f(x) = y
Definition
A function $f : X → Y$ is called bijective if it is both injective and surjective.
def my_bijective {X Y : Type u} (f : X → Y) := injective f ∧ surjective f
Remark. Although we have defined some lovely properties for our functions, it turns out that these definitions are already defined in the LEAN maths library. So while our effort might be wasted, we can now use some theorems already written without going through them ourselves!
Bijectivity and Composition
Theorem
Let $f : X → Y$ and $g : Y → Z$ be functions, then if $f$ and $g$ are both injective, then so is $g ∘ f$.
theorem both_injective
(X Y Z : Type u) (f : X → Y) (g : Y → Z) : injective f ∧ injective g → injective (g ∘ f) :=
Proof
QED.
Suppose that $f$ and $g$ are injective functions, we need to show that $g ∘ f$ is also injective, i.e. if $(g ∘ f)(a) = (g ∘ f)(b)$, then $a = b$.
intros h a b ha,
X Y Z : Type u,
f : X → Y,
g : Y → Z
⊢ injective f ∧ injective g → injective (g ∘ f)
X Y Z : Type u,
f : X → Y,
g : Y → Z,
h : injective f ∧ injective g,
a b : X,
ha : (g ∘ f) a = (g ∘ f) b
⊢ a = b
Since $g$ is injective, we have $f(a) = f(b)$.
apply h.left,
X Y Z : Type u,
f : X → Y,
g : Y → Z,
h : injective f ∧ injective g,
a b : X,
ha : (g ∘ f) a = (g ∘ f) b
⊢ a = b
X Y Z : Type u,
f : X → Y,
g : Y → Z,
h : injective f ∧ injective g,
a b : X,
ha : (g ∘ f) a = (g ∘ f) b
⊢ f a = f b
Similarly, since $f$ is injective, $a = b$, which is exactly what we wanted!
apply h.right,
X Y Z : Type u,
f : X → Y,
g : Y → Z,
h : injective f ∧ injective g,
a b : X,
ha : (g ∘ f) a = (g ∘ f) b
⊢ f a = f b
X Y Z : Type u,
f : X → Y,
g : Y → Z,
h : injective f ∧ injective g,
a b : X,
ha : (g ∘ f) a = (g ∘ f) b
⊢ g (f a) = g (f b)
assumption
X Y Z : Type u,
f : X → Y,
g : Y → Z,
h : injective f ∧ injective g,
a b : X,
ha : (g ∘ f) a = (g ∘ f) b
⊢ g (f a) = g (f b)
X Y Z : Type u,
f : X → Y,
g : Y → Z,
h : injective f ∧ injective g,
a b : X,
ha : (g ∘ f) a = (g ∘ f) b
⊢ g (f a) = g (f b)
Remark. Notice that in step 2, LEAN knew that by definition, $(g ∘ f)(x) = g(f(x))$, so we have $g (f(a)) = g (f(b))$, how smart is that!
Theorem
Let $f : X → Y$ and $g : Y → Z$ be functions, then if $f$ and $g$ are both surjective, then so is $g ∘ f$.
theorem both_surjective
(X Y Z : Type u) (f : X → Y) (g : Y → Z) : surjective f ∧ surjective g → surjective (g ∘ f) :=
Proof
QED.
Suppose that $f$ and $g$ are surjective functions, we need to show that $g ∘ f$ is also surjective, i.e. $∀ z ∈ Z, ∃ x ∈ X, (g ∘ f)(x) = z$.
intros h z,
X Y Z : Type u,
f : X → Y,
g : Y → Z
⊢ surjective f ∧ surjective g → surjective (g ∘ f)
X Y Z : Type u,
f : X → Y,
g : Y → Z,
h : surjective f ∧ surjective g,
z : Z
⊢ ∃ (a : X), (g ∘ f) a = z
Since $g$ is surjective, there is a $y ∈ Y$ such that $g(y) = z$.
have ha : ∃ y : Y, g(y) = z, apply h.right,
X Y Z : Type u,
f : X → Y,
g : Y → Z,
h : surjective f ∧ surjective g,
z : Z
⊢ ∃ (a : X), (g ∘ f) a = z
X Y Z : Type u,
f : X → Y,
g : Y → Z,
h : surjective f ∧ surjective g,
z : Z,
ha : ∃ (y : Y), g y = z
⊢ ∃ (a : X), (g ∘ f) a = z
cases ha with y hy,
X Y Z : Type u,
f : X → Y,
g : Y → Z,
h : surjective f ∧ surjective g,
z : Z,
ha : ∃ (y : Y), g y = z
⊢ ∃ (a : X), (g ∘ f) a = z
X Y Z : Type u,
f : X → Y,
g : Y → Z,
h : surjective f ∧ surjective g,
z : Z,
y : Y,
hy : g y = z
⊢ ∃ (a : X), (g ∘ f) a = z
Similarly, as $f$ is surjective, there is a $x ∈ X$ such that $f(x) = y$.
have hb : ∃ x : X, f(x) = y, apply h.left,
X Y Z : Type u,
f : X → Y,
g : Y → Z,
h : surjective f ∧ surjective g,
z : Z,
y : Y,
hy : g y = z
⊢ ∃ (a : X), (g ∘ f) a = z
X Y Z : Type u,
f : X → Y,
g : Y → Z,
h : surjective f ∧ surjective g,
z : Z,
y : Y,
hy : g y = z,
hb : ∃ (x : X), f x = y
⊢ ∃ (a : X), (g ∘ f) a = z
cases hb with x hx,
X Y Z : Type u,
f : X → Y,
g : Y → Z,
h : surjective f ∧ surjective g,
z : Z,
y : Y,
hy : g y = z,
hb : ∃ (x : X), f x = y
⊢ ∃ (a : X), (g ∘ f) a = z
X Y Z : Type u,
f : X → Y,
g : Y → Z,
h : surjective f ∧ surjective g,
z : Z,
y : Y,
hy : g y = z,
x : X,
hx : f x = y
⊢ ∃ (a : X), (g ∘ f) a = z
But by definition, $(g ∘ f)(x) = g(f(x)) = g(y) = z$ So we are done!
existsi x,
X Y Z : Type u,
f : X → Y,
g : Y → Z,
h : surjective f ∧ surjective g,
z : Z,
y : Y,
hy : g y = z,
x : X,
hx : f x = y
⊢ ∃ (a : X), (g ∘ f) a = z
X Y Z : Type u,
f : X → Y,
g : Y → Z,
h : surjective f ∧ surjective g,
z : Z,
y : Y,
hy : g y = z,
x : X,
hx : f x = y
⊢ (g ∘ f) x = z
rwa [←hy, ←hx]
X Y Z : Type u,
f : X → Y,
g : Y → Z,
h : surjective f ∧ surjective g,
z : Z,
y : Y,
hy : g y = z,
x : X,
hx : f x = y
⊢ (g ∘ f) x = z
X Y Z : Type u,
f : X → Y,
g : Y → Z,
h : surjective f ∧ surjective g,
z : Z,
y : Y,
hy : g y = z,
x : X,
hx : f x = y
⊢ (g ∘ f) x = z
Theorem
Let $f : X → Y$ and $g : Y → Z$ be functions, then if $f$ and $g$ are both bijective, then so is $g ∘ f$.
theorem both_bijective
(X Y Z : Type u) (f : X → Y) (g : Y → Z) : bijective f ∧ bijective g → bijective (g ∘ f) :=
Proof
QED.
Since $f$ and $g$ are bijective, they are also injective and surjective.
rintro ⟨⟨hfi, hfs⟩, hgi, hgs⟩,
X Y Z : Type u,
f : X → Y,
g : Y → Z
⊢ bijective f ∧ bijective g → bijective (g ∘ f)
X Y Z : Type u,
f : X → Y,
g : Y → Z,
hfi : injective f,
hfs : surjective f,
hgi : injective g,
hgs : surjective g
⊢ bijective (g ∘ f)
split,
X Y Z : Type u,
f : X → Y,
g : Y → Z,
hfi : injective f,
hfs : surjective f,
hgi : injective g,
hgs : surjective g
⊢ bijective (g ∘ f)
2 goals
X Y Z : Type u,
f : X → Y,
g : Y → Z,
hfi : injective f,
hfs : surjective f,
hgi : injective g,
hgs : surjective g
⊢ injective (g ∘ f)
X Y Z : Type u,
f : X → Y,
g : Y → Z,
hfi : injective f,
hfs : surjective f,
hgi : injective g,
hgs : surjective g
⊢ surjective (g ∘ f)
But since $f$ and $g$ are injective, $g ∘ f$ is injective by our previous theorem.
apply both_injective,
2 goals
X Y Z : Type u,
f : X → Y,
g : Y → Z,
hfi : injective f,
hfs : surjective f,
hgi : injective g,
hgs : surjective g
⊢ injective (g ∘ f)
X Y Z : Type u,
f : X → Y,
g : Y → Z,
hfi : injective f,
hfs : surjective f,
hgi : injective g,
hgs : surjective g
⊢ surjective (g ∘ f)
2 goals
X Y Z : Type u,
f : X → Y,
g : Y → Z,
hfi : injective f,
hfs : surjective f,
hgi : injective g,
hgs : surjective g
⊢ injective f ∧ injective g
X Y Z : Type u,
f : X → Y,
g : Y → Z,
hfi : injective f,
hfs : surjective f,
hgi : injective g,
hgs : surjective g
⊢ surjective (g ∘ f)
split,
2 goals
X Y Z : Type u,
f : X → Y,
g : Y → Z,
hfi : injective f,
hfs : surjective f,
hgi : injective g,
hgs : surjective g
⊢ injective f ∧ injective g
X Y Z : Type u,
f : X → Y,
g : Y → Z,
hfi : injective f,
hfs : surjective f,
hgi : injective g,
hgs : surjective g
⊢ surjective (g ∘ f)
3 goals
X Y Z : Type u,
f : X → Y,
g : Y → Z,
hfi : injective f,
hfs : surjective f,
hgi : injective g,
hgs : surjective g
⊢ injective f
X Y Z : Type u,
f : X → Y,
g : Y → Z,
hfi : injective f,
hfs : surjective f,
hgi : injective g,
hgs : surjective g
⊢ injective g
X Y Z : Type u,
f : X → Y,
g : Y → Z,
hfi : injective f,
hfs : surjective f,
hgi : injective g,
hgs : surjective g
⊢ surjective (g ∘ f)
repeat {assumption},
3 goals
X Y Z : Type u,
f : X → Y,
g : Y → Z,
hfi : injective f,
hfs : surjective f,
hgi : injective g,
hgs : surjective g
⊢ injective f
X Y Z : Type u,
f : X → Y,
g : Y → Z,
hfi : injective f,
hfs : surjective f,
hgi : injective g,
hgs : surjective g
⊢ injective g
X Y Z : Type u,
f : X → Y,
g : Y → Z,
hfi : injective f,
hfs : surjective f,
hgi : injective g,
hgs : surjective g
⊢ surjective (g ∘ f)
X Y Z : Type u,
f : X → Y,
g : Y → Z,
hfi : injective f,
hfs : surjective f,
hgi : injective g,
hgs : surjective g
⊢ surjective (g ∘ f)
Similarly, since $f$ and $g$ surjective, $g ∘ f$ is surjective.
apply both_surjective,
X Y Z : Type u,
f : X → Y,
g : Y → Z,
hfi : injective f,
hfs : surjective f,
hgi : injective g,
hgs : surjective g
⊢ surjective (g ∘ f)
X Y Z : Type u,
f : X → Y,
g : Y → Z,
hfi : injective f,
hfs : surjective f,
hgi : injective g,
hgs : surjective g
⊢ surjective f ∧ surjective g
split,
X Y Z : Type u,
f : X → Y,
g : Y → Z,
hfi : injective f,
hfs : surjective f,
hgi : injective g,
hgs : surjective g
⊢ surjective f ∧ surjective g
2 goals
X Y Z : Type u,
f : X → Y,
g : Y → Z,
hfi : injective f,
hfs : surjective f,
hgi : injective g,
hgs : surjective g
⊢ surjective f
X Y Z : Type u,
f : X → Y,
g : Y → Z,
hfi : injective f,
hfs : surjective f,
hgi : injective g,
hgs : surjective g
⊢ surjective g
Hence, since $g ∘ f$ is injective and surjective, $g ∘ f$ is bijective.
repeat {assumption}
2 goals
X Y Z : Type u,
f : X → Y,
g : Y → Z,
hfi : injective f,
hfs : surjective f,
hgi : injective g,
hgs : surjective g
⊢ surjective f
X Y Z : Type u,
f : X → Y,
g : Y → Z,
hfi : injective f,
hfs : surjective f,
hgi : injective g,
hgs : surjective g
⊢ surjective g
2 goals
X Y Z : Type u,
f : X → Y,
g : Y → Z,
hfi : injective f,
hfs : surjective f,
hgi : injective g,
hgs : surjective g
⊢ surjective f
X Y Z : Type u,
f : X → Y,
g : Y → Z,
hfi : injective f,
hfs : surjective f,
hgi : injective g,
hgs : surjective g
⊢ surjective g
2.4 Inverses
Definition
By digging through $\tt{functions}$, it turns out that the brilliant people of LEAN has not yet defined two sided inverse as the time of writting this.
So let's define $g : Y → X$ to be the two sided inverse of $f : X → Y$ if and only if $∀ x ∈ X, (g ∘ f)(x) = x$ and $∀ y ∈ Y, (f ∘ g)(y) = y$.
def two_sided_inverse {X Y : Type u} (f : X → Y) (g : Y → X) := (∀ x : X, (g ∘ f)(x) = x) ∧ (∀ y : Y, (f ∘ g)(y) = y)
Theorem
A function $f : X → Y$ has a two-sided inverse if and only if it is a bijection.
theorem exist_two_sided_inverse
(X Y : Type u) (f : X → Y) : (∃ g : Y → X, two_sided_inverse f g) ↔ bijective f :=
Proof
QED.
Again, since the question is in the form of 'if and only if', we need to prove both sides of the implications.
split,
X Y : Type u,
f : X → Y
⊢ (∃ (g : Y → X), two_sided_inverse f g) ↔ bijective f
2 goals
X Y : Type u,
f : X → Y
⊢ (∃ (g : Y → X), two_sided_inverse f g) → bijective f
X Y : Type u,
f : X → Y
⊢ bijective f → (∃ (g : Y → X), two_sided_inverse f g)
$(⇒)$ Suppose the function $f : X → Y$ has a two sided inverse $g$, we need to show that $f$ is bijective, i.e. it is injective and surjective.
rintro ⟨g, ⟨hlinv, hrinv⟩⟩,
2 goals
X Y : Type u,
f : X → Y
⊢ (∃ (g : Y → X), two_sided_inverse f g) → bijective f
X Y : Type u,
f : X → Y
⊢ bijective f → (∃ (g : Y → X), two_sided_inverse f g)
2 goals
X Y : Type u,
f : X → Y,
g : Y → X,
hlinv : ∀ (x : X), (g ∘ f) x = x,
hrinv : ∀ (y : Y), (f ∘ g) y = y
⊢ bijective f
X Y : Type u,
f : X → Y
⊢ bijective f → (∃ (g : Y → X), two_sided_inverse f g)
So lets first show that $f$ is injective.
have hfinj : injective f,
2 goals
X Y : Type u,
f : X → Y,
g : Y → X,
hlinv : ∀ (x : X), (g ∘ f) x = x,
hrinv : ∀ (y : Y), (f ∘ g) y = y
⊢ bijective f
X Y : Type u,
f : X → Y
⊢ bijective f → (∃ (g : Y → X), two_sided_inverse f g)
3 goals
X Y : Type u,
f : X → Y,
g : Y → X,
hlinv : ∀ (x : X), (g ∘ f) x = x,
hrinv : ∀ (y : Y), (f ∘ g) y = y
⊢ injective f
X Y : Type u,
f : X → Y,
g : Y → X,
hlinv : ∀ (x : X), (g ∘ f) x = x,
hrinv : ∀ (y : Y), (f ∘ g) y = y,
hfinj : injective f
⊢ bijective f
X Y : Type u,
f : X → Y
⊢ bijective f → (∃ (g : Y → X), two_sided_inverse f g)
Suppose we have $f(p) = f(q)$ for some $p q ∈ X$, then $f$ is injective if $p = q$.
intros p q hf,
3 goals
X Y : Type u,
f : X → Y,
g : Y → X,
hlinv : ∀ (x : X), (g ∘ f) x = x,
hrinv : ∀ (y : Y), (f ∘ g) y = y
⊢ injective f
X Y : Type u,
f : X → Y,
g : Y → X,
hlinv : ∀ (x : X), (g ∘ f) x = x,
hrinv : ∀ (y : Y), (f ∘ g) y = y,
hfinj : injective f
⊢ bijective f
X Y : Type u,
f : X → Y
⊢ bijective f → (∃ (g : Y → X), two_sided_inverse f g)
3 goals
X Y : Type u,
f : X → Y,
g : Y → X,
hlinv : ∀ (x : X), (g ∘ f) x = x,
hrinv : ∀ (y : Y), (f ∘ g) y = y,
p q : X,
hf : f p = f q
⊢ p = q
X Y : Type u,
f : X → Y,
g : Y → X,
hlinv : ∀ (x : X), (g ∘ f) x = x,
hrinv : ∀ (y : Y), (f ∘ g) y = y,
hfinj : injective f
⊢ bijective f
X Y : Type u,
f : X → Y
⊢ bijective f → (∃ (g : Y → X), two_sided_inverse f g)
Since $f(p) = f(q)$, we have $g(f(p)) = g(f(q))$.
replace hf : g (f p) = g (f q), rw hf,
3 goals
X Y : Type u,
f : X → Y,
g : Y → X,
hlinv : ∀ (x : X), (g ∘ f) x = x,
hrinv : ∀ (y : Y), (f ∘ g) y = y,
p q : X,
hf : f p = f q
⊢ p = q
X Y : Type u,
f : X → Y,
g : Y → X,
hlinv : ∀ (x : X), (g ∘ f) x = x,
hrinv : ∀ (y : Y), (f ∘ g) y = y,
hfinj : injective f
⊢ bijective f
X Y : Type u,
f : X → Y
⊢ bijective f → (∃ (g : Y → X), two_sided_inverse f g)
3 goals
X Y : Type u,
f : X → Y,
g : Y → X,
hlinv : ∀ (x : X), (g ∘ f) x = x,
hrinv : ∀ (y : Y), (f ∘ g) y = y,
p q : X,
hf : g (f p) = g (f q)
⊢ p = q
X Y : Type u,
f : X → Y,
g : Y → X,
hlinv : ∀ (x : X), (g ∘ f) x = x,
hrinv : ∀ (y : Y), (f ∘ g) y = y,
hfinj : injective f
⊢ bijective f
X Y : Type u,
f : X → Y
⊢ bijective f → (∃ (g : Y → X), two_sided_inverse f g)
But since $g$ is a double sided inverse of $f$, $∀ x ∈ X, g(f(x)) = x$, hence $p = g(f(p))= g(f(q)) = q$ which is exactly what we need!
have ha : g (f p) = p := hlinv p,
3 goals
X Y : Type u,
f : X → Y,
g : Y → X,
hlinv : ∀ (x : X), (g ∘ f) x = x,
hrinv : ∀ (y : Y), (f ∘ g) y = y,
p q : X,
hf : g (f p) = g (f q)
⊢ p = q
X Y : Type u,
f : X → Y,
g : Y → X,
hlinv : ∀ (x : X), (g ∘ f) x = x,
hrinv : ∀ (y : Y), (f ∘ g) y = y,
hfinj : injective f
⊢ bijective f
X Y : Type u,
f : X → Y
⊢ bijective f → (∃ (g : Y → X), two_sided_inverse f g)
3 goals
X Y : Type u,
f : X → Y,
g : Y → X,
hlinv : ∀ (x : X), (g ∘ f) x = x,
hrinv : ∀ (y : Y), (f ∘ g) y = y,
p q : X,
hf : g (f p) = g (f q),
ha : g (f p) = p
⊢ p = q
X Y : Type u,
f : X → Y,
g : Y → X,
hlinv : ∀ (x : X), (g ∘ f) x = x,
hrinv : ∀ (y : Y), (f ∘ g) y = y,
hfinj : injective f
⊢ bijective f
X Y : Type u,
f : X → Y
⊢ bijective f → (∃ (g : Y → X), two_sided_inverse f g)
have hb : g (f q) = q := hlinv q,
3 goals
X Y : Type u,
f : X → Y,
g : Y → X,
hlinv : ∀ (x : X), (g ∘ f) x = x,
hrinv : ∀ (y : Y), (f ∘ g) y = y,
p q : X,
hf : g (f p) = g (f q),
ha : g (f p) = p
⊢ p = q
X Y : Type u,
f : X → Y,
g : Y → X,
hlinv : ∀ (x : X), (g ∘ f) x = x,
hrinv : ∀ (y : Y), (f ∘ g) y = y,
hfinj : injective f
⊢ bijective f
X Y : Type u,
f : X → Y
⊢ bijective f → (∃ (g : Y → X), two_sided_inverse f g)
3 goals
X Y : Type u,
f : X → Y,
g : Y → X,
hlinv : ∀ (x : X), (g ∘ f) x = x,
hrinv : ∀ (y : Y), (f ∘ g) y = y,
p q : X,
hf : g (f p) = g (f q),
ha : g (f p) = p,
hb : g (f q) = q
⊢ p = q
X Y : Type u,
f : X → Y,
g : Y → X,
hlinv : ∀ (x : X), (g ∘ f) x = x,
hrinv : ∀ (y : Y), (f ∘ g) y = y,
hfinj : injective f
⊢ bijective f
X Y : Type u,
f : X → Y
⊢ bijective f → (∃ (g : Y → X), two_sided_inverse f g)
rw [ha, hb] at hf,
3 goals
X Y : Type u,
f : X → Y,
g : Y → X,
hlinv : ∀ (x : X), (g ∘ f) x = x,
hrinv : ∀ (y : Y), (f ∘ g) y = y,
p q : X,
hf : g (f p) = g (f q),
ha : g (f p) = p,
hb : g (f q) = q
⊢ p = q
X Y : Type u,
f : X → Y,
g : Y → X,
hlinv : ∀ (x : X), (g ∘ f) x = x,
hrinv : ∀ (y : Y), (f ∘ g) y = y,
hfinj : injective f
⊢ bijective f
X Y : Type u,
f : X → Y
⊢ bijective f → (∃ (g : Y → X), two_sided_inverse f g)
3 goals
X Y : Type u,
f : X → Y,
g : Y → X,
hlinv : ∀ (x : X), (g ∘ f) x = x,
hrinv : ∀ (y : Y), (f ∘ g) y = y,
p q : X,
ha : g (f p) = p,
hb : g (f q) = q,
hf : p = q
⊢ p = q
X Y : Type u,
f : X → Y,
g : Y → X,
hlinv : ∀ (x : X), (g ∘ f) x = x,
hrinv : ∀ (y : Y), (f ∘ g) y = y,
hfinj : injective f
⊢ bijective f
X Y : Type u,
f : X → Y
⊢ bijective f → (∃ (g : Y → X), two_sided_inverse f g)
assumption,
3 goals
X Y : Type u,
f : X → Y,
g : Y → X,
hlinv : ∀ (x : X), (g ∘ f) x = x,
hrinv : ∀ (y : Y), (f ∘ g) y = y,
p q : X,
ha : g (f p) = p,
hb : g (f q) = q,
hf : p = q
⊢ p = q
X Y : Type u,
f : X → Y,
g : Y → X,
hlinv : ∀ (x : X), (g ∘ f) x = x,
hrinv : ∀ (y : Y), (f ∘ g) y = y,
hfinj : injective f
⊢ bijective f
X Y : Type u,
f : X → Y
⊢ bijective f → (∃ (g : Y → X), two_sided_inverse f g)
2 goals
X Y : Type u,
f : X → Y,
g : Y → X,
hlinv : ∀ (x : X), (g ∘ f) x = x,
hrinv : ∀ (y : Y), (f ∘ g) y = y,
hfinj : injective f
⊢ bijective f
X Y : Type u,
f : X → Y
⊢ bijective f → (∃ (g : Y → X), two_sided_inverse f g)
Now we need to show that $f$ is surjective, i.e. $∀ y ∈ Y, ∃ x ∈ X, f(x) = y$.
have hfbsur : surjective f,
2 goals
X Y : Type u,
f : X → Y,
g : Y → X,
hlinv : ∀ (x : X), (g ∘ f) x = x,
hrinv : ∀ (y : Y), (f ∘ g) y = y,
hfinj : injective f
⊢ bijective f
X Y : Type u,
f : X → Y
⊢ bijective f → (∃ (g : Y → X), two_sided_inverse f g)
3 goals
X Y : Type u,
f : X → Y,
g : Y → X,
hlinv : ∀ (x : X), (g ∘ f) x = x,
hrinv : ∀ (y : Y), (f ∘ g) y = y,
hfinj : injective f
⊢ surjective f
X Y : Type u,
f : X → Y,
g : Y → X,
hlinv : ∀ (x : X), (g ∘ f) x = x,
hrinv : ∀ (y : Y), (f ∘ g) y = y,
hfinj : injective f,
hfbsur : surjective f
⊢ bijective f
X Y : Type u,
f : X → Y
⊢ bijective f → (∃ (g : Y → X), two_sided_inverse f g)
intro y,
3 goals
X Y : Type u,
f : X → Y,
g : Y → X,
hlinv : ∀ (x : X), (g ∘ f) x = x,
hrinv : ∀ (y : Y), (f ∘ g) y = y,
hfinj : injective f
⊢ surjective f
X Y : Type u,
f : X → Y,
g : Y → X,
hlinv : ∀ (x : X), (g ∘ f) x = x,
hrinv : ∀ (y : Y), (f ∘ g) y = y,
hfinj : injective f,
hfbsur : surjective f
⊢ bijective f
X Y : Type u,
f : X → Y
⊢ bijective f → (∃ (g : Y → X), two_sided_inverse f g)
3 goals
X Y : Type u,
f : X → Y,
g : Y → X,
hlinv : ∀ (x : X), (g ∘ f) x = x,
hrinv : ∀ (y : Y), (f ∘ g) y = y,
hfinj : injective f,
y : Y
⊢ ∃ (a : X), f a = y
X Y : Type u,
f : X → Y,
g : Y → X,
hlinv : ∀ (x : X), (g ∘ f) x = x,
hrinv : ∀ (y : Y), (f ∘ g) y = y,
hfinj : injective f,
hfbsur : surjective f
⊢ bijective f
X Y : Type u,
f : X → Y
⊢ bijective f → (∃ (g : Y → X), two_sided_inverse f g)
Since we have $g(y) ∈ X$, suppose we choose $x$ to be $g(y)$.
existsi g y,
3 goals
X Y : Type u,
f : X → Y,
g : Y → X,
hlinv : ∀ (x : X), (g ∘ f) x = x,
hrinv : ∀ (y : Y), (f ∘ g) y = y,
hfinj : injective f,
y : Y
⊢ ∃ (a : X), f a = y
X Y : Type u,
f : X → Y,
g : Y → X,
hlinv : ∀ (x : X), (g ∘ f) x = x,
hrinv : ∀ (y : Y), (f ∘ g) y = y,
hfinj : injective f,
hfbsur : surjective f
⊢ bijective f
X Y : Type u,
f : X → Y
⊢ bijective f → (∃ (g : Y → X), two_sided_inverse f g)
3 goals
X Y : Type u,
f : X → Y,
g : Y → X,
hlinv : ∀ (x : X), (g ∘ f) x = x,
hrinv : ∀ (y : Y), (f ∘ g) y = y,
hfinj : injective f,
y : Y
⊢ f (g y) = y
X Y : Type u,
f : X → Y,
g : Y → X,
hlinv : ∀ (x : X), (g ∘ f) x = x,
hrinv : ∀ (y : Y), (f ∘ g) y = y,
hfinj : injective f,
hfbsur : surjective f
⊢ bijective f
X Y : Type u,
f : X → Y
⊢ bijective f → (∃ (g : Y → X), two_sided_inverse f g)
But, as $g$ is a double inverse of $f$, $f(g(y)) = y$ which is exactly what we need!
exact hrinv y,
3 goals
X Y : Type u,
f : X → Y,
g : Y → X,
hlinv : ∀ (x : X), (g ∘ f) x = x,
hrinv : ∀ (y : Y), (f ∘ g) y = y,
hfinj : injective f,
y : Y
⊢ f (g y) = y
X Y : Type u,
f : X → Y,
g : Y → X,
hlinv : ∀ (x : X), (g ∘ f) x = x,
hrinv : ∀ (y : Y), (f ∘ g) y = y,
hfinj : injective f,
hfbsur : surjective f
⊢ bijective f
X Y : Type u,
f : X → Y
⊢ bijective f → (∃ (g : Y → X), two_sided_inverse f g)
2 goals
X Y : Type u,
f : X → Y,
g : Y → X,
hlinv : ∀ (x : X), (g ∘ f) x = x,
hrinv : ∀ (y : Y), (f ∘ g) y = y,
hfinj : injective f,
hfbsur : surjective f
⊢ bijective f
X Y : Type u,
f : X → Y
⊢ bijective f → (∃ (g : Y → X), two_sided_inverse f g)
Thus, as $f$ is both injective and surjective, $f$ is bijective!
split,
2 goals
X Y : Type u,
f : X → Y,
g : Y → X,
hlinv : ∀ (x : X), (g ∘ f) x = x,
hrinv : ∀ (y : Y), (f ∘ g) y = y,
hfinj : injective f,
hfbsur : surjective f
⊢ bijective f
X Y : Type u,
f : X → Y
⊢ bijective f → (∃ (g : Y → X), two_sided_inverse f g)
3 goals
X Y : Type u,
f : X → Y,
g : Y → X,
hlinv : ∀ (x : X), (g ∘ f) x = x,
hrinv : ∀ (y : Y), (f ∘ g) y = y,
hfinj : injective f,
hfbsur : surjective f
⊢ injective f
X Y : Type u,
f : X → Y,
g : Y → X,
hlinv : ∀ (x : X), (g ∘ f) x = x,
hrinv : ∀ (y : Y), (f ∘ g) y = y,
hfinj : injective f,
hfbsur : surjective f
⊢ surjective f
X Y : Type u,
f : X → Y
⊢ bijective f → (∃ (g : Y → X), two_sided_inverse f g)
all_goals {try {assumption}},
3 goals
X Y : Type u,
f : X → Y,
g : Y → X,
hlinv : ∀ (x : X), (g ∘ f) x = x,
hrinv : ∀ (y : Y), (f ∘ g) y = y,
hfinj : injective f,
hfbsur : surjective f
⊢ injective f
X Y : Type u,
f : X → Y,
g : Y → X,
hlinv : ∀ (x : X), (g ∘ f) x = x,
hrinv : ∀ (y : Y), (f ∘ g) y = y,
hfinj : injective f,
hfbsur : surjective f
⊢ surjective f
X Y : Type u,
f : X → Y
⊢ bijective f → (∃ (g : Y → X), two_sided_inverse f g)
X Y : Type u,
f : X → Y
⊢ bijective f → (∃ (g : Y → X), two_sided_inverse f g)
$(⇐)$ Now lets prove the reverse implication, i.e. if $f$ is bijective, then $f$ has a two-sided inverse.
rintro ⟨hfinj, hfsur⟩,
X Y : Type u,
f : X → Y
⊢ bijective f → (∃ (g : Y → X), two_sided_inverse f g)
X Y : Type u,
f : X → Y,
hfinj : injective f,
hfsur : surjective f
⊢ ∃ (g : Y → X), two_sided_inverse f g
Since $f$ is surjective, $∀ y ∈ Y, ∃ x ∈ X$ such that $f(x) = y$, lets choose this $x$ to be our output of $g(y)$.
choose g hg using hfsur,
X Y : Type u,
f : X → Y,
hfinj : injective f,
hfsur : surjective f
⊢ ∃ (g : Y → X), two_sided_inverse f g
X Y : Type u,
f : X → Y,
hfinj : injective f,
g : Y → X,
hg : ∀ (b : Y), f (g b) = b
⊢ ∃ (g : Y → X), two_sided_inverse f g
existsi g,
X Y : Type u,
f : X → Y,
hfinj : injective f,
g : Y → X,
hg : ∀ (b : Y), f (g b) = b
⊢ ∃ (g : Y → X), two_sided_inverse f g
X Y : Type u,
f : X → Y,
hfinj : injective f,
g : Y → X,
hg : ∀ (b : Y), f (g b) = b
⊢ two_sided_inverse f g
Now we need to show that $g$ is a double sided inverse of $f$ so let's first show that $g$ is a left inverse of $f$.
split,
X Y : Type u,
f : X → Y,
hfinj : injective f,
g : Y → X,
hg : ∀ (b : Y), f (g b) = b
⊢ two_sided_inverse f g
2 goals
X Y : Type u,
f : X → Y,
hfinj : injective f,
g : Y → X,
hg : ∀ (b : Y), f (g b) = b
⊢ ∀ (x : X), (g ∘ f) x = x
X Y : Type u,
f : X → Y,
hfinj : injective f,
g : Y → X,
hg : ∀ (b : Y), f (g b) = b
⊢ ∀ (y : Y), (f ∘ g) y = y
intro a,
2 goals
X Y : Type u,
f : X → Y,
hfinj : injective f,
g : Y → X,
hg : ∀ (b : Y), f (g b) = b
⊢ ∀ (x : X), (g ∘ f) x = x
X Y : Type u,
f : X → Y,
hfinj : injective f,
g : Y → X,
hg : ∀ (b : Y), f (g b) = b
⊢ ∀ (y : Y), (f ∘ g) y = y
2 goals
X Y : Type u,
f : X → Y,
hfinj : injective f,
g : Y → X,
hg : ∀ (b : Y), f (g b) = b,
a : X
⊢ (g ∘ f) a = a
X Y : Type u,
f : X → Y,
hfinj : injective f,
g : Y → X,
hg : ∀ (b : Y), f (g b) = b
⊢ ∀ (y : Y), (f ∘ g) y = y
Consider that since, by definition of $g$, $∀ y ∈ Y, f(g(y)) = y$ we have $f(g(f(a))) = f(a)$,
have ha : f (g (f a)) = f a,
2 goals
X Y : Type u,
f : X → Y,
hfinj : injective f,
g : Y → X,
hg : ∀ (b : Y), f (g b) = b,
a : X
⊢ (g ∘ f) a = a
X Y : Type u,
f : X → Y,
hfinj : injective f,
g : Y → X,
hg : ∀ (b : Y), f (g b) = b
⊢ ∀ (y : Y), (f ∘ g) y = y
3 goals
X Y : Type u,
f : X → Y,
hfinj : injective f,
g : Y → X,
hg : ∀ (b : Y), f (g b) = b,
a : X
⊢ f (g (f a)) = f a
X Y : Type u,
f : X → Y,
hfinj : injective f,
g : Y → X,
hg : ∀ (b : Y), f (g b) = b,
a : X,
ha : f (g (f a)) = f a
⊢ (g ∘ f) a = a
X Y : Type u,
f : X → Y,
hfinj : injective f,
g : Y → X,
hg : ∀ (b : Y), f (g b) = b
⊢ ∀ (y : Y), (f ∘ g) y = y
rw hg (f a),
3 goals
X Y : Type u,
f : X → Y,
hfinj : injective f,
g : Y → X,
hg : ∀ (b : Y), f (g b) = b,
a : X
⊢ f (g (f a)) = f a
X Y : Type u,
f : X → Y,
hfinj : injective f,
g : Y → X,
hg : ∀ (b : Y), f (g b) = b,
a : X,
ha : f (g (f a)) = f a
⊢ (g ∘ f) a = a
X Y : Type u,
f : X → Y,
hfinj : injective f,
g : Y → X,
hg : ∀ (b : Y), f (g b) = b
⊢ ∀ (y : Y), (f ∘ g) y = y
2 goals
X Y : Type u,
f : X → Y,
hfinj : injective f,
g : Y → X,
hg : ∀ (b : Y), f (g b) = b,
a : X,
ha : f (g (f a)) = f a
⊢ (g ∘ f) a = a
X Y : Type u,
f : X → Y,
hfinj : injective f,
g : Y → X,
hg : ∀ (b : Y), f (g b) = b
⊢ ∀ (y : Y), (f ∘ g) y = y
therefore, as $f$ is injective, we have $f(g(f(a))) = f(a) ⇒ g(f(a)) = f(a)$. Thus, $g$ is a left inverse of $f$.
exact hfinj ha,
2 goals
X Y : Type u,
f : X → Y,
hfinj : injective f,
g : Y → X,
hg : ∀ (b : Y), f (g b) = b,
a : X,
ha : f (g (f a)) = f a
⊢ (g ∘ f) a = a
X Y : Type u,
f : X → Y,
hfinj : injective f,
g : Y → X,
hg : ∀ (b : Y), f (g b) = b
⊢ ∀ (y : Y), (f ∘ g) y = y
X Y : Type u,
f : X → Y,
hfinj : injective f,
g : Y → X,
hg : ∀ (b : Y), f (g b) = b
⊢ ∀ (y : Y), (f ∘ g) y = y
Now, all we have left to prove is that $g$ is a right inverse of $f$. But that is true by definition, so we are done!
assumption
X Y : Type u,
f : X → Y,
hfinj : injective f,
g : Y → X,
hg : ∀ (b : Y), f (g b) = b
⊢ ∀ (y : Y), (f ∘ g) y = y
X Y : Type u,
f : X → Y,
hfinj : injective f,
g : Y → X,
hg : ∀ (b : Y), f (g b) = b
⊢ ∀ (y : Y), (f ∘ g) y = y
2.5 Binary Relations
Definition
A binary relation $R$ on a set $X$ is a function $R : X^2 → \tt{Prop}$.
def bin_rel (X) := X → X → Prop
2.6 Common Predicates on Binary Relations
Definition
A binary relation $R$ on $X$ is called relfexive if $∀ x ∈ X, R(x, x)$.
def reflexive (r : bin_rel X) := ∀ x : X, r x x
Theorem
$≤$ is reflexive on $ℝ$.
@[simp] theorem le_refl : reflexive ((≤) : ℝ → ℝ → Prop) :=
Proof
QED.
To prove that the binary relation $≤$ on $ℝ$ is reflexive, we need to show given arbitary $x ∈ ℝ$, $x ≤ x$.
intro,
⊢ reflexive has_le.le
x : ℝ
⊢ x ≤ x
But this obviously true, so we're done!
refl
x : ℝ
⊢ x ≤ x
x : ℝ
⊢ x ≤ x
Definition
A binary relation $R$ on $X$ is called symmetric if $∀a, b ∈ X, R(a, b) ⇒ R(b, a)$.
def symmetric (r : bin_rel X) := ∀ x y : X, r x y → r y x
Theorem
$=$ is symmetric on $ℝ$.
theorem eq_symm : symmetric ((=) : ℝ → ℝ → Prop) :=
Proof
QED.
To prove that $=$ is a symmetric binary relation on $ℝ$, we need to show that given $x = y$, $y = x$.
intros x y h,
⊢ symmetric eq
x y : ℝ,
h : x = y
⊢ y = x
But if $x = y$, then we can re-write $y$ as $x$ and $x$ as $y$, thus, $y = x$.
rwa h
x y : ℝ,
h : x = y
⊢ y = x
x y : ℝ,
h : x = y
⊢ y = x
Definition
A binary relation $R$ on $X$ is called antisymmetric if $∀ a, b ∈ X, R(a, b) ∧ R(b, a) ⇒ a = b$.
def antisymmetric (r : bin_rel X) := ∀ x y : X, r x y ∧ r y x → x = y
Theorem
$≤$ is anti-symmetric on $R$.
@[simp] theorem le_antisymm : antisymmetric ((≤) : ℝ → ℝ → Prop) :=
Proof
QED.
Suppose we have $x, y ∈ ℝ$ where $x ≤ y$ and $y ≤ x$, then we need to show that $x = y$.
intros x y h,
⊢ antisymmetric has_le.le
x y : ℝ,
h : x ≤ y ∧ y ≤ x
⊢ x = y
have h0 : (x < y ∨ x = y) ∧ (y < x ∨ y = x),
x y : ℝ,
h : x ≤ y ∧ y ≤ x
⊢ x = y
2 goals
x y : ℝ,
h : x ≤ y ∧ y ≤ x
⊢ (x < y ∨ x = y) ∧ (y < x ∨ y = x)
x y : ℝ,
h : x ≤ y ∧ y ≤ x,
h0 : (x < y ∨ x = y) ∧ (y < x ∨ y = x)
⊢ x = y
repeat {rw ←le_iff_lt_or_eq}, assumption,
2 goals
x y : ℝ,
h : x ≤ y ∧ y ≤ x
⊢ (x < y ∨ x = y) ∧ (y < x ∨ y = x)
x y : ℝ,
h : x ≤ y ∧ y ≤ x,
h0 : (x < y ∨ x = y) ∧ (y < x ∨ y = x)
⊢ x = y
x y : ℝ,
h : x ≤ y ∧ y ≤ x,
h0 : (x < y ∨ x = y) ∧ (y < x ∨ y = x)
⊢ x = y
By the trichotomy axioms, either $x < y$, $y < x$ or $x = y$.
cases lt_trichotomy x y with ha hb,
x y : ℝ,
h : x ≤ y ∧ y ≤ x,
h0 : (x < y ∨ x = y) ∧ (y < x ∨ y = x)
⊢ x = y
2 goals
case or.inl
x y : ℝ,
h : x ≤ y ∧ y ≤ x,
h0 : (x < y ∨ x = y) ∧ (y < x ∨ y = x),
ha : x < y
⊢ x = y
case or.inr
x y : ℝ,
h : x ≤ y ∧ y ≤ x,
h0 : (x < y ∨ x = y) ∧ (y < x ∨ y = x),
hb : x = y ∨ y < x
⊢ x = y
Let's first suppose that $x < y$, then obviously $¬ (y < x)$. But since we have $y ≤ x$, $x$ must therefore equal to $y$!
{suffices : ¬ (y < x),
2 goals
case or.inl
x y : ℝ,
h : x ≤ y ∧ y ≤ x,
h0 : (x < y ∨ x = y) ∧ (y < x ∨ y = x),
ha : x < y
⊢ x = y
case or.inr
x y : ℝ,
h : x ≤ y ∧ y ≤ x,
h0 : (x < y ∨ x = y) ∧ (y < x ∨ y = x),
hb : x = y ∨ y < x
⊢ x = y
2 goals
x y : ℝ,
h : x ≤ y ∧ y ≤ x,
h0 : (x < y ∨ x = y) ∧ (y < x ∨ y = x),
ha : x < y,
this : ¬y < x
⊢ x = y
x y : ℝ,
h : x ≤ y ∧ y ≤ x,
h0 : (x < y ∨ x = y) ∧ (y < x ∨ y = x),
ha : x < y
⊢ ¬y < x
cases h0.right with hc hd, contradiction, rwa hd,
2 goals
x y : ℝ,
h : x ≤ y ∧ y ≤ x,
h0 : (x < y ∨ x = y) ∧ (y < x ∨ y = x),
ha : x < y,
this : ¬y < x
⊢ x = y
x y : ℝ,
h : x ≤ y ∧ y ≤ x,
h0 : (x < y ∨ x = y) ∧ (y < x ∨ y = x),
ha : x < y
⊢ ¬y < x
x y : ℝ,
h : x ≤ y ∧ y ≤ x,
h0 : (x < y ∨ x = y) ∧ (y < x ∨ y = x),
ha : x < y
⊢ ¬y < x
simp, from h.left},
x y : ℝ,
h : x ≤ y ∧ y ≤ x,
h0 : (x < y ∨ x = y) ∧ (y < x ∨ y = x),
ha : x < y
⊢ ¬y < x
case or.inr
x y : ℝ,
h : x ≤ y ∧ y ≤ x,
h0 : (x < y ∨ x = y) ∧ (y < x ∨ y = x),
hb : x = y ∨ y < x
⊢ x = y
{cases hb with he hf,
case or.inr
x y : ℝ,
h : x ≤ y ∧ y ≤ x,
h0 : (x < y ∨ x = y) ∧ (y < x ∨ y = x),
hb : x = y ∨ y < x
⊢ x = y
2 goals
case or.inl
x y : ℝ,
h : x ≤ y ∧ y ≤ x,
h0 : (x < y ∨ x = y) ∧ (y < x ∨ y = x),
he : x = y
⊢ x = y
case or.inr
x y : ℝ,
h : x ≤ y ∧ y ≤ x,
h0 : (x < y ∨ x = y) ∧ (y < x ∨ y = x),
hf : y < x
⊢ x = y
Let's now consider the other two cases. If $x = y$ then there is nothing left to prove so lets suppose $y < x$.
{assumption},
2 goals
case or.inl
x y : ℝ,
h : x ≤ y ∧ y ≤ x,
h0 : (x < y ∨ x = y) ∧ (y < x ∨ y = x),
he : x = y
⊢ x = y
case or.inr
x y : ℝ,
h : x ≤ y ∧ y ≤ x,
h0 : (x < y ∨ x = y) ∧ (y < x ∨ y = x),
hf : y < x
⊢ x = y
case or.inr
x y : ℝ,
h : x ≤ y ∧ y ≤ x,
h0 : (x < y ∨ x = y) ∧ (y < x ∨ y = x),
hf : y < x
⊢ x = y
Similar to before, $(y < x) ⇒ ¬ (x < y)$. But $(x ≤ y)$, therefore $x = y$!
{suffices : ¬ (x < y),
case or.inr
x y : ℝ,
h : x ≤ y ∧ y ≤ x,
h0 : (x < y ∨ x = y) ∧ (y < x ∨ y = x),
hf : y < x
⊢ x = y
2 goals
x y : ℝ,
h : x ≤ y ∧ y ≤ x,
h0 : (x < y ∨ x = y) ∧ (y < x ∨ y = x),
hf : y < x,
this : ¬x < y
⊢ x = y
x y : ℝ,
h : x ≤ y ∧ y ≤ x,
h0 : (x < y ∨ x = y) ∧ (y < x ∨ y = x),
hf : y < x
⊢ ¬x < y
cases h0.left with hc hd, contradiction, rwa hd,
2 goals
x y : ℝ,
h : x ≤ y ∧ y ≤ x,
h0 : (x < y ∨ x = y) ∧ (y < x ∨ y = x),
hf : y < x,
this : ¬x < y
⊢ x = y
x y : ℝ,
h : x ≤ y ∧ y ≤ x,
h0 : (x < y ∨ x = y) ∧ (y < x ∨ y = x),
hf : y < x
⊢ ¬x < y
x y : ℝ,
h : x ≤ y ∧ y ≤ x,
h0 : (x < y ∨ x = y) ∧ (y < x ∨ y = x),
hf : y < x
⊢ ¬x < y
simp, from h.right}
x y : ℝ,
h : x ≤ y ∧ y ≤ x,
h0 : (x < y ∨ x = y) ∧ (y < x ∨ y = x),
hf : y < x
⊢ ¬x < y
no goals
}
no goals
no goals
Remark. Notice that in the above proof I used a lot of curly bracket. This will limit the tactic state to only show the the goal within the brackets and thus also limit clutter. Read more about how to structure LEAN proofs nicely here.
Definition
A binary relation $R$ on $X$ is called transitive if $∀ a, b, c ∈ X, R(a, b) ∧ R(b, c) ⇒ R(a, c)$.
def transitive (r : bin_rel X) := ∀ x y z : X, r x y ∧ r y z → r x z
Theorem
$⇒$ is transitive on the set of propositions.
theorem imply_trans : transitive ((→) : Prop → Prop → Prop) :=
Proof
QED.
Let $P, Q, R$ be propositions such that $P ⇒ Q$ and $Q ⇒ R$. We then need to prove that $P ⇒ R$. Suppose $P$ is true.
intros P Q R h hp,
⊢ transitive (λ (_x _y : Prop), _x → _y)
P Q R : Prop,
h : (λ (_x _y : Prop), _x → _y) P Q ∧ (λ (_x _y : Prop), _x → _y) Q R,
hp : P
⊢ R
Then as $P ⇒ Q$, $Q$ must also be true. And again as $Q ⇒ R$, $R$ must also be true. Thus $P ⇒ R$, and we are done!
from h.right (h.left hp)
P Q R : Prop,
h : (λ (_x _y : Prop), _x → _y) P Q ∧ (λ (_x _y : Prop), _x → _y) Q R,
hp : P
⊢ R
P Q R : Prop,
h : (λ (_x _y : Prop), _x → _y) P Q ∧ (λ (_x _y : Prop), _x → _y) Q R,
hp : P
⊢ R
Theorem
$≤$ is transitive on $ℝ$.
@[simp] theorem le_trans : transitive ((≤) : ℝ → ℝ → Prop) :=
Proof
QED.
This one is a bit tricky and require us to delve into how ordering is defined on the reals in LEAN.
intros x y z h,
⊢ transitive has_le.le
x y z : ℝ,
h : x ≤ y ∧ y ≤ z
⊢ x ≤ z
However, with the power that is mathlib, we see that there is something called $\tt{le_trans}$, so why don't we just steal that for our use here!
from le_trans h.left h.right
x y z : ℝ,
h : x ≤ y ∧ y ≤ z
⊢ x ≤ z
x y z : ℝ,
h : x ≤ y ∧ y ≤ z
⊢ x ≤ z
2.7 Partial and Total Orders
Let $R$ be a binary relation on the set $X$.
Definition
We call $R$ a partial order if it is reflexive, antisymmetric, and transitive.
def partial_order (r : bin_rel X) := reflexive r ∧ antisymmetric r ∧ transitive r
Definition
We call $R$ total if $∀ a, b ∈ X, R(a, b) ∨ R(b, a)$.
def total (r : bin_rel X) := ∀ x y : X, r x y ∨ r y x
Definition
We call $R$ a total order if it is total and a partial order.
def total_order (r : bin_rel X) := partial_order r ∧ total r
Let's now prove that $≤$ is a total order. As we already have already proven that $≤$ is reflexive, symmetric, and transitive, i.e. its a partial order, we only need to show $≤$ is total to prove that $≤$ is a total order.
Lemma
$≤$ is total on $ℝ$.
@[simp] theorem le_total : total ((≤) : ℝ → ℝ → Prop) :=
Proof
QED.
Suppose we have $x, y ∈ ℝ$, by the trichotomy axiom, either $x < y$, $y < x$ or $x = y$.
intros x y,
⊢ total has_le.le
x y : ℝ
⊢ x ≤ y ∨ y ≤ x
cases lt_trichotomy x y,
x y : ℝ
⊢ x ≤ y ∨ y ≤ x
2 goals
case or.inl
x y : ℝ,
h : x < y
⊢ x ≤ y ∨ y ≤ x
case or.inr
x y : ℝ,
h : x = y ∨ y < x
⊢ x ≤ y ∨ y ≤ x
If $x < y$ then $x ≤ y$.
repeat {rw le_iff_lt_or_eq},
2 goals
case or.inl
x y : ℝ,
h : x < y
⊢ x ≤ y ∨ y ≤ x
case or.inr
x y : ℝ,
h : x = y ∨ y < x
⊢ x ≤ y ∨ y ≤ x
2 goals
case or.inl
x y : ℝ,
h : x < y
⊢ (x < y ∨ x = y) ∨ y < x ∨ y = x
case or.inr
x y : ℝ,
h : x = y ∨ y < x
⊢ (x < y ∨ x = y) ∨ y < x ∨ y = x
{left, left, assumption},
2 goals
case or.inl
x y : ℝ,
h : x < y
⊢ (x < y ∨ x = y) ∨ y < x ∨ y = x
case or.inr
x y : ℝ,
h : x = y ∨ y < x
⊢ (x < y ∨ x = y) ∨ y < x ∨ y = x
case or.inr
x y : ℝ,
h : x = y ∨ y < x
⊢ (x < y ∨ x = y) ∨ y < x ∨ y = x
If $x = y$ then also $x ≤ y$. However, if $y > x$, then we have $y ≤ x$. Thus, by considering all the cases, we see either $x ≤ y$ or $y ≤ x$.
{cases h, repeat { {left, assumption} <|> right <|> assumption }, rwa h}
case or.inr
x y : ℝ,
h : x = y ∨ y < x
⊢ (x < y ∨ x = y) ∨ y < x ∨ y = x
no goals
Remark. The last line of this LEAN proof uses something called $\tt{tactic combinators}$. Read about is here.
Theorem
$≤$ is a total order on $ℝ$.
theorem le_total_order : total_order ((≤) : ℝ → ℝ → Prop) :=
Proof
QED.
As $≤$ is a partial order and is total, it is a total order!
repeat {split},
⊢ total_order has_le.le
4 goals
⊢ reflexive has_le.le
⊢ antisymmetric has_le.le
⊢ transitive has_le.le
⊢ total has_le.le
repeat {simp}
4 goals
⊢ reflexive has_le.le
⊢ antisymmetric has_le.le
⊢ transitive has_le.le
⊢ total has_le.le
4 goals
⊢ reflexive has_le.le
⊢ antisymmetric has_le.le
⊢ transitive has_le.le
⊢ total has_le.le
Remark. Notice how I tagged some of the theorems above with $\tt{@[simp]}$? This tells LEAN to try to uses theses theorems whenever I use the tactive $\tt{simp}$. Read more about it here.
2.7 Equivalence Relations
Definition
A binary relation $R$ on the set $X$ is called an equivalence relation if it is reflexive, symmetric, and transitive.
def equivalence (r : bin_rel X) := reflexive r ∧ symmetric r ∧ transitive r
We'll present some examples of equivalence relations below.
Definition
Suppose we define a binary relation $R(m, n)$, $m, n ∈ ℤ$, where $R(m, n)$ is true if and only if $m - n$ is even.
def R (m n : ℤ) := 2 ∣ (m - n)
Lemma
(1) $R$ is reflexive.
lemma R_refl : reflexive R :=
Proof
QED.
We have for any $m ∈ ℝ$, $m - m = 0$.
intro,
⊢ reflexive R
x : ℤ
⊢ R x x
unfold R,
x : ℤ
⊢ R x x
x : ℤ
⊢ 2 ∣ x - x
As $2 ∣ 0$, we have $R(m, m)$ is true!
simp,
x : ℤ
⊢ 2 ∣ x - x
no goals
Lemma
(2) $R$ is symmetric.
lemma R_symm : symmetric R :=
Proof
QED.
Suppose we have $m, n ∈ ℝ$ such that $R(m, n)$ is true.
intros m n,
⊢ symmetric R
m n : ℤ
⊢ R m n → R n m
As $R(m, n)$ implies $2 ∣ m - n$, $∃ x ∈ ℤ, 2 x = m - n$.
rintro ⟨x, hx⟩,
m n : ℤ
⊢ R m n → R n m
m n x : ℤ,
hx : m - n = 2 * x
⊢ R n m
existsi -x,
m n x : ℤ,
hx : m - n = 2 * x
⊢ R n m
m n x : ℤ,
hx : m - n = 2 * x
⊢ n - m = 2 * -x
But this means $2 (-x) = n - m$, i.e. $2 ∣ n - m$, thus $R(n, m)$ is also true!
simp, rw ←hx, ring,
m n x : ℤ,
hx : m - n = 2 * x
⊢ n - m = 2 * -x
no goals
Lemma
(3) $R$ is transitive.
lemma R_trans : transitive R :=
Proof
QED.
Suppose we have $l, m, n ∈ ℝ$ such that $R(m, l)$ and $R(l, n)$, we need to show $R(m, n)$ is true.
intros l m n,
⊢ transitive R
l m n : ℤ
⊢ R l m ∧ R m n → R l n
Since $R(m, l)$ and $R(l, n)$ implies $2 ∣ m - l$ and $2 ∣ l - n$, $∃ x, y ∈ ℤ, 2 x = m - l, 2 y = l - n$.
rintro ⟨⟨x, hx⟩, ⟨y, hy⟩⟩,
l m n : ℤ
⊢ R l m ∧ R m n → R l n
l m n x : ℤ,
hx : l - m = 2 * x,
y : ℤ,
hy : m - n = 2 * y
⊢ R l n
existsi x + y,
l m n x : ℤ,
hx : l - m = 2 * x,
y : ℤ,
hy : m - n = 2 * y
⊢ R l n
l m n x : ℤ,
hx : l - m = 2 * x,
y : ℤ,
hy : m - n = 2 * y
⊢ l - n = 2 * (x + y)
But then $2 (x + y) = 2 x + 2 y = m - l + l - n = m - n$. Thus $2 ∣ m - n$, i.e. $R(m, n)$.
ring, rw [←hx, ←hy], ring,
l m n x : ℤ,
hx : l - m = 2 * x,
y : ℤ,
hy : m - n = 2 * y
⊢ l - n = 2 * (x + y)
no goals
Theorem
$R$ is an equivalence relation.
theorem R_equiv : equivalence R :=
Proof
QED.
This follows directly from lemma (1), (2), and (3).
repeat {split},
⊢ equivalence R
3 goals
⊢ reflexive R
⊢ symmetric R
⊢ transitive R
{from R_refl},
3 goals
⊢ reflexive R
⊢ symmetric R
⊢ transitive R
2 goals
⊢ symmetric R
⊢ transitive R
{from R_symm},
2 goals
⊢ symmetric R
⊢ transitive R
⊢ transitive R
{from R_trans}
⊢ transitive R
no goals
Definition
Let $X$ be a set of sets, where $A, B ∈ X$. Let's define $<\mathtt{\sim}$ such that $A <~ B$ if an only if $∃ g: A → B$, $g$ is an injection.
def brel (A B : Type*) := ∃ g : A → B, function.bijective g
infix ` <~ `: 50 := brel
Lemma
$<\mathtt{\sim}$ is reflexive.
@[simp] lemma brel_refl : reflexive (<~) :=
Proof
QED.
To prove $<\mathtt{\sim}$ is reflexive we need to show there exists a bijection between a set $X$ and itself.
intro X,
⊢ reflexive brel
X : Type u_1
⊢ X <~ X
Luckily, we can simply choose the identity function!
let g : X → X := id,
X : Type u_1
⊢ X <~ X
X : Type u_1,
g : X → X := id
⊢ X <~ X
existsi g,
X : Type u_1,
g : X → X := id
⊢ X <~ X
X : Type u_1,
g : X → X := id
⊢ bijective g
Since the identity function is bijective, $<\mathtt{\sim}$ is reflexive as required.
from function.bijective_id
X : Type u_1,
g : X → X := id
⊢ bijective g
X : Type u_1,
g : X → X := id
⊢ bijective g
Lemma
$<\mathtt{\sim}$ is symmetric.
@[simp] lemma brel_symm : symmetric (<~) :=
Proof
QED.
To prove $<\mathtt{\sim}$ is symmetric we need to show that, for sets $X, Y$, $X <~ Y ⇒ Y <~ X$.
intros X Y,
⊢ symmetric brel
X Y : Type u_1
⊢ X <~ Y → Y <~ X
Suppose $X <~ Y$, then by definition, $∃ f : X → Y$, where $f$ is bijective.
rintro ⟨f, hf⟩,
X Y : Type u_1
⊢ X <~ Y → Y <~ X
X Y : Type u_1,
f : X → Y,
hf : bijective f
⊢ Y <~ X
As proven ealier, $f$ is bijective implies $f$ has a two sided inverse $g$, let's choose that as our function.
have hg : ∃ g : Y → X, two_sided_inverse f g,
X Y : Type u_1,
f : X → Y,
hf : bijective f
⊢ Y <~ X
2 goals
X Y : Type u_1,
f : X → Y,
hf : bijective f
⊢ ∃ (g : Y → X), two_sided_inverse f g
X Y : Type u_1,
f : X → Y,
hf : bijective f,
hg : ∃ (g : Y → X), two_sided_inverse f g
⊢ Y <~ X
{rwa exist_two_sided_inverse
2 goals
X Y : Type u_1,
f : X → Y,
hf : bijective f
⊢ ∃ (g : Y → X), two_sided_inverse f g
X Y : Type u_1,
f : X → Y,
hf : bijective f,
hg : ∃ (g : Y → X), two_sided_inverse f g
⊢ Y <~ X
2 goals
X Y : Type u_1,
f : X → Y,
hf : bijective f
⊢ ∃ (g : Y → X), two_sided_inverse f g
X Y : Type u_1,
f : X → Y,
hf : bijective f,
hg : ∃ (g : Y → X), two_sided_inverse f g
⊢ Y <~ X
},
2 goals
X Y : Type u_1,
f : X → Y,
hf : bijective f
⊢ ∃ (g : Y → X), two_sided_inverse f g
X Y : Type u_1,
f : X → Y,
hf : bijective f,
hg : ∃ (g : Y → X), two_sided_inverse f g
⊢ Y <~ X
X Y : Type u_1,
f : X → Y,
hf : bijective f,
hg : ∃ (g : Y → X), two_sided_inverse f g
⊢ Y <~ X
{cases hg with g hg,
X Y : Type u_1,
f : X → Y,
hf : bijective f,
hg : ∃ (g : Y → X), two_sided_inverse f g
⊢ Y <~ X
X Y : Type u_1,
f : X → Y,
hf : bijective f,
g : Y → X,
hg : two_sided_inverse f g
⊢ Y <~ X
existsi g,
X Y : Type u_1,
f : X → Y,
hf : bijective f,
g : Y → X,
hg : two_sided_inverse f g
⊢ Y <~ X
X Y : Type u_1,
f : X → Y,
hf : bijective f,
g : Y → X,
hg : two_sided_inverse f g
⊢ bijective g
Since $g$ is bijective if and only if $g$ has a two sided inverse, it suffices to prove that such an inverse exist.
rw ←exist_two_sided_inverse,
X Y : Type u_1,
f : X → Y,
hf : bijective f,
g : Y → X,
hg : two_sided_inverse f g
⊢ bijective g
X Y : Type u_1,
f : X → Y,
hf : bijective f,
g : Y → X,
hg : two_sided_inverse f g
⊢ ∃ (g_1 : X → Y), two_sided_inverse g g_1
But as $g$ is the two sided inverse of $f$ by construction, we have $f$ is the two sided inverse of $g$ by definition, thus such an inverse does exist!
existsi f,
X Y : Type u_1,
f : X → Y,
hf : bijective f,
g : Y → X,
hg : two_sided_inverse f g
⊢ ∃ (g_1 : X → Y), two_sided_inverse g g_1
X Y : Type u_1,
f : X → Y,
hf : bijective f,
g : Y → X,
hg : two_sided_inverse f g
⊢ two_sided_inverse g f
split,
X Y : Type u_1,
f : X → Y,
hf : bijective f,
g : Y → X,
hg : two_sided_inverse f g
⊢ two_sided_inverse g f
2 goals
X Y : Type u_1,
f : X → Y,
hf : bijective f,
g : Y → X,
hg : two_sided_inverse f g
⊢ ∀ (x : Y), (f ∘ g) x = x
X Y : Type u_1,
f : X → Y,
hf : bijective f,
g : Y → X,
hg : two_sided_inverse f g
⊢ ∀ (y : X), (g ∘ f) y = y
{from hg.right},
2 goals
X Y : Type u_1,
f : X → Y,
hf : bijective f,
g : Y → X,
hg : two_sided_inverse f g
⊢ ∀ (x : Y), (f ∘ g) x = x
X Y : Type u_1,
f : X → Y,
hf : bijective f,
g : Y → X,
hg : two_sided_inverse f g
⊢ ∀ (y : X), (g ∘ f) y = y
X Y : Type u_1,
f : X → Y,
hf : bijective f,
g : Y → X,
hg : two_sided_inverse f g
⊢ ∀ (y : X), (g ∘ f) y = y
{from hg.left}
X Y : Type u_1,
f : X → Y,
hf : bijective f,
g : Y → X,
hg : two_sided_inverse f g
⊢ ∀ (y : X), (g ∘ f) y = y
no goals
}
no goals
no goals
Lemma
$<\mathtt{\sim}$ is transitive.
@[simp] lemma brel_trans : transitive (<~) :=
Proof
QED.
Given three sets $X, Y, Z$ where $X <~ Y$ and $Y <~ Z$ we need to show that $X <~ Z$.
intros X Y Z,
⊢ transitive brel
X Y Z : Type u_1
⊢ X <~ Y ∧ Y <~ Z → X <~ Z
Since $X <~ Y$ and $Y <~ Z$ there exists bijective functions $f : X → Y$ and $g : Y → Z$.
rintro ⟨⟨f, hf⟩, g, hg⟩,
X Y Z : Type u_1
⊢ X <~ Y ∧ Y <~ Z → X <~ Z
X Y Z : Type u_1,
f : X → Y,
hf : bijective f,
g : Y → Z,
hg : bijective g
⊢ X <~ Z
But as proven ealier, the composition of two bijective functions is also bijective. Thus, $g ∘ f : X → Z$ is a bijective function which is exactly what we need!
existsi (g ∘ f),
X Y Z : Type u_1,
f : X → Y,
hf : bijective f,
g : Y → Z,
hg : bijective g
⊢ X <~ Z
X Y Z : Type u_1,
f : X → Y,
hf : bijective f,
g : Y → Z,
hg : bijective g
⊢ bijective (g ∘ f)
apply both_bijective,
X Y Z : Type u_1,
f : X → Y,
hf : bijective f,
g : Y → Z,
hg : bijective g
⊢ bijective (g ∘ f)
X Y Z : Type u_1,
f : X → Y,
hf : bijective f,
g : Y → Z,
hg : bijective g
⊢ bijective f ∧ bijective g
split, repeat {assumption}
X Y Z : Type u_1,
f : X → Y,
hf : bijective f,
g : Y → Z,
hg : bijective g
⊢ bijective f ∧ bijective g
2 goals
X Y Z : Type u_1,
f : X → Y,
hf : bijective f,
g : Y → Z,
hg : bijective g
⊢ bijective f
X Y Z : Type u_1,
f : X → Y,
hf : bijective f,
g : Y → Z,
hg : bijective g
⊢ bijective g
With that, we can conclude that $<\mathtt{\sim}$ is an equivalence relation!
Theorem
$<\mathtt{\sim}$ is an equivalence relation
theorem brel_equiv : equivalence (<~) :=
Proof
QED.
This follows as $<\mathtt{\sim}$ is reflexive, symmetric and transitive!
repeat {split},
⊢ equivalence brel
3 goals
⊢ reflexive brel
⊢ symmetric brel
⊢ transitive brel
repeat {simp}
3 goals
⊢ reflexive brel
⊢ symmetric brel
⊢ transitive brel
3 goals
⊢ reflexive brel
⊢ symmetric brel
⊢ transitive brel
Exercise. I have defined one more binary relation $\mathtt{\sim}>$. Can you try to prove it here?
2.9 Quotients and Equivalence Classes
2.9.1 Equivalence Classes
Definition
Let $X$ be a set and let $\mathtt{\sim}$ be an equivalence relation on $X$. Let $s ∈ X$ be an arbitrary element. We define the equivalence class of $s$, written $cl(s)$ as $cl(s) = \{x ∈ X ∣ s \mathtt{\sim} x\}.
def cls (r : bin_rel X) (s : X) := {x : X | r s x}
Lemma
(1) Let $X$ be a set and let $R$ be an equivalence relation on $X$. Then, for $s, t ∈ X$, $R(s, t) ⇒ cl(t) ⊆ cl(s)$.
lemma class_relate_lem_a
(s t : X) (R : bin_rel X) (h : equivalence R) : R s t → cls R t ⊆ cls R s :=
Proof
QED.
Given that $R$ is an equivalence relation, we know that it is reflexive, symmetric and transitive.
rcases h with ⟨href, ⟨hsym, htrans⟩⟩,
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R
⊢ R s t → cls R t ⊆ cls R s
X : Type u,
s t : X,
R : bin_rel X,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R
⊢ R s t → cls R t ⊆ cls R s
Thus, given an element $x$ in $cl(t)$ (i.e. $R(t, x)$ is true), we have, by transitivit, $R(s, x)$.
intros ha x hb,
X : Type u,
s t : X,
R : bin_rel X,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R
⊢ R s t → cls R t ⊆ cls R s
X : Type u,
s t : X,
R : bin_rel X,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R,
ha : R s t,
x : X,
hb : x ∈ cls R t
⊢ x ∈ cls R s
have hc : R t x := hb,
X : Type u,
s t : X,
R : bin_rel X,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R,
ha : R s t,
x : X,
hb : x ∈ cls R t
⊢ x ∈ cls R s
X : Type u,
s t : X,
R : bin_rel X,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R,
ha : R s t,
x : X,
hb : x ∈ cls R t,
hc : R t x
⊢ x ∈ cls R s
replace hc : R s t ∧ R t x, by {split, repeat {assumption}},
X : Type u,
s t : X,
R : bin_rel X,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R,
ha : R s t,
x : X,
hb : x ∈ cls R t,
hc : R t x
⊢ x ∈ cls R s
X : Type u,
s t : X,
R : bin_rel X,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R,
ha : R s t,
x : X,
hb : x ∈ cls R t,
hc : R s t ∧ R t x
⊢ x ∈ cls R s
replace hc : R s x := htrans s t x hc,
X : Type u,
s t : X,
R : bin_rel X,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R,
ha : R s t,
x : X,
hb : x ∈ cls R t,
hc : R s t ∧ R t x
⊢ x ∈ cls R s
X : Type u,
s t : X,
R : bin_rel X,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R,
ha : R s t,
x : X,
hb : x ∈ cls R t,
hc : R s x
⊢ x ∈ cls R s
Hence $x ∈ cl(s)$ by definition.
from hc
X : Type u,
s t : X,
R : bin_rel X,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R,
ha : R s t,
x : X,
hb : x ∈ cls R t,
hc : R s x
⊢ x ∈ cls R s
X : Type u,
s t : X,
R : bin_rel X,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R,
ha : R s t,
x : X,
hb : x ∈ cls R t,
hc : R s x
⊢ x ∈ cls R s
With lemma (1) in place, it is quite easy to see that, not only is $cl(t) ⊆ cl(s)$, in fact, $cl(t) = cl(s)$.
Lemma
(2) Let $X$ be a set and let $R$ be an equivalence relation on $X$. Then, for $s, t ∈ X$, $R(s, t) ⇒ cl(t) = cl(s)$.
lemma class_relate_lem_b
(s t : X) (R : bin_rel X) (h : equivalence R) : R s t → cls R t = cls R s :=
Proof
QED.
By lemma (1), $cl(t) ⊆ cl(s), and thus, we only need to prove that $cl(s) ⊆ cl(t)$ in order for $cl(t) = cl(s)$.
intro h0,
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R
⊢ R s t → cls R t = cls R s
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
h0 : R s t
⊢ cls R t = cls R s
rw le_antisymm_iff,
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
h0 : R s t
⊢ cls R t = cls R s
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
h0 : R s t
⊢ cls R t ≤ cls R s ∧ cls R s ≤ cls R t
split,
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
h0 : R s t
⊢ cls R t ≤ cls R s ∧ cls R s ≤ cls R t
2 goals
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
h0 : R s t
⊢ cls R t ≤ cls R s
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
h0 : R s t
⊢ cls R s ≤ cls R t
all_goals {apply class_relate_lem_a,
2 goals
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
h0 : R s t
⊢ cls R t ≤ cls R s
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
h0 : R s t
⊢ cls R s ≤ cls R t
2 goals
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
h0 : R s t
⊢ equivalence R
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
h0 : R s t
⊢ R s t
repeat {assumption}
2 goals
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
h0 : R s t
⊢ equivalence R
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
h0 : R s t
⊢ R s t
2 goals
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
h0 : R s t
⊢ equivalence R
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
h0 : R s t
⊢ R s t
},
2 goals
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
h0 : R s t
⊢ equivalence R
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
h0 : R s t
⊢ R s t
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
h0 : R s t
⊢ R t s
But, since $R$ is and equivalence relation, it is symmetric.
{rcases h with ⟨href, ⟨hsym, htrans⟩⟩,
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
h0 : R s t
⊢ R t s
X : Type u,
s t : X,
R : bin_rel X,
h0 : R s t,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R
⊢ R t s
Hence, $R(s, t) ↔ R(t, s)$ which by lemma (1) implies $cl(s) ⊆ cl(t)$ as required.
from hsym s t h0
X : Type u,
s t : X,
R : bin_rel X,
h0 : R s t,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R
⊢ R t s
X : Type u,
s t : X,
R : bin_rel X,
h0 : R s t,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R
⊢ R t s
}
X : Type u,
s t : X,
R : bin_rel X,
h0 : R s t,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R
⊢ R t s
no goals
Lemma
(3) Let $X$ be a set and let $R$ be an equivalence relation on $X$. Then, for $s, t ∈ X$, $¬ R(s, t) ⇒ cl(t) ∩ cl(s) = ∅$.
lemma class_not_relate
(s t : X) (R : bin_rel X) (h : equivalence R) : ¬ R s t → cls R t ∩ cls R s = ∅ :=
Proof
QED.
We prove by contradiction. Suppose $cl(t) ∩ cl(s) ≠ ∅$.
intros ha hb,
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
this : cls R t ∩ cls R s = ∅ ↔ ¬¬cls R t ∩ cls R s = ∅
⊢ ¬R s t → ¬¬cls R t ∩ cls R s = ∅
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
this : cls R t ∩ cls R s = ∅ ↔ ¬¬cls R t ∩ cls R s = ∅,
ha : ¬R s t,
hb : ¬cls R t ∩ cls R s = ∅
⊢ false
Then, there must be some $x$ in $cl(t) ∩ cl(s)$.
have hx : ∃ x, x ∈ cls R t ∩ cls R s := set.exists_mem_of_ne_empty hb,
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
this : cls R t ∩ cls R s = ∅ ↔ ¬¬cls R t ∩ cls R s = ∅,
ha : ¬R s t,
hb : ¬cls R t ∩ cls R s = ∅
⊢ false
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
this : cls R t ∩ cls R s = ∅ ↔ ¬¬cls R t ∩ cls R s = ∅,
ha : ¬R s t,
hb : ¬cls R t ∩ cls R s = ∅,
hx : ∃ (x : X), x ∈ cls R t ∩ cls R s
⊢ false
rcases hx with ⟨x, ⟨hα, hβ⟩⟩,
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
this : cls R t ∩ cls R s = ∅ ↔ ¬¬cls R t ∩ cls R s = ∅,
ha : ¬R s t,
hb : ¬cls R t ∩ cls R s = ∅,
hx : ∃ (x : X), x ∈ cls R t ∩ cls R s
⊢ false
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
this : cls R t ∩ cls R s = ∅ ↔ ¬¬cls R t ∩ cls R s = ∅,
ha : ¬R s t,
hb : ¬cls R t ∩ cls R s = ∅,
x : X,
hα : x ∈ cls R t,
hβ : x ∈ cls R s
⊢ false
Thus, by definition, $R(t, x)$ and $R(s, t)$ must both be true!
rcases h with ⟨href, ⟨hsym, htrans⟩⟩,
X : Type u,
s t : X,
R : bin_rel X,
h : equivalence R,
this : cls R t ∩ cls R s = ∅ ↔ ¬¬cls R t ∩ cls R s = ∅,
ha : ¬R s t,
hb : ¬cls R t ∩ cls R s = ∅,
x : X,
hα : x ∈ cls R t,
hβ : x ∈ cls R s
⊢ false
X : Type u,
s t : X,
R : bin_rel X,
this : cls R t ∩ cls R s = ∅ ↔ ¬¬cls R t ∩ cls R s = ∅,
ha : ¬R s t,
hb : ¬cls R t ∩ cls R s = ∅,
x : X,
hα : x ∈ cls R t,
hβ : x ∈ cls R s,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R
⊢ false
have hc : R s x ∧ R x t, by {split,
X : Type u,
s t : X,
R : bin_rel X,
this : cls R t ∩ cls R s = ∅ ↔ ¬¬cls R t ∩ cls R s = ∅,
ha : ¬R s t,
hb : ¬cls R t ∩ cls R s = ∅,
x : X,
hα : x ∈ cls R t,
hβ : x ∈ cls R s,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R
⊢ false
2 goals
X : Type u,
s t : X,
R : bin_rel X,
this : cls R t ∩ cls R s = ∅ ↔ ¬¬cls R t ∩ cls R s = ∅,
ha : ¬R s t,
hb : ¬cls R t ∩ cls R s = ∅,
x : X,
hα : x ∈ cls R t,
hβ : x ∈ cls R s,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R
⊢ R s x
X : Type u,
s t : X,
R : bin_rel X,
this : cls R t ∩ cls R s = ∅ ↔ ¬¬cls R t ∩ cls R s = ∅,
ha : ¬R s t,
hb : ¬cls R t ∩ cls R s = ∅,
x : X,
hα : x ∈ cls R t,
hβ : x ∈ cls R s,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R
⊢ R x t
from hβ,
2 goals
X : Type u,
s t : X,
R : bin_rel X,
this : cls R t ∩ cls R s = ∅ ↔ ¬¬cls R t ∩ cls R s = ∅,
ha : ¬R s t,
hb : ¬cls R t ∩ cls R s = ∅,
x : X,
hα : x ∈ cls R t,
hβ : x ∈ cls R s,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R
⊢ R s x
X : Type u,
s t : X,
R : bin_rel X,
this : cls R t ∩ cls R s = ∅ ↔ ¬¬cls R t ∩ cls R s = ∅,
ha : ¬R s t,
hb : ¬cls R t ∩ cls R s = ∅,
x : X,
hα : x ∈ cls R t,
hβ : x ∈ cls R s,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R
⊢ R x t
X : Type u,
s t : X,
R : bin_rel X,
this : cls R t ∩ cls R s = ∅ ↔ ¬¬cls R t ∩ cls R s = ∅,
ha : ¬R s t,
hb : ¬cls R t ∩ cls R s = ∅,
x : X,
hα : x ∈ cls R t,
hβ : x ∈ cls R s,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R
⊢ R x t
apply hsym, from hα},
X : Type u,
s t : X,
R : bin_rel X,
this : cls R t ∩ cls R s = ∅ ↔ ¬¬cls R t ∩ cls R s = ∅,
ha : ¬R s t,
hb : ¬cls R t ∩ cls R s = ∅,
x : X,
hα : x ∈ cls R t,
hβ : x ∈ cls R s,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R
⊢ R x t
X : Type u,
s t : X,
R : bin_rel X,
this : cls R t ∩ cls R s = ∅ ↔ ¬¬cls R t ∩ cls R s = ∅,
ha : ¬R s t,
hb : ¬cls R t ∩ cls R s = ∅,
x : X,
hα : x ∈ cls R t,
hβ : x ∈ cls R s,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R,
hc : R s x ∧ R x t
⊢ false
But this means $R(s, t)$ must also be true by transitivity, a contradiction to $¬ R(s, t)$!
have hd : R s t, by {from htrans s x t hc},
X : Type u,
s t : X,
R : bin_rel X,
this : cls R t ∩ cls R s = ∅ ↔ ¬¬cls R t ∩ cls R s = ∅,
ha : ¬R s t,
hb : ¬cls R t ∩ cls R s = ∅,
x : X,
hα : x ∈ cls R t,
hβ : x ∈ cls R s,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R,
hc : R s x ∧ R x t
⊢ false
X : Type u,
s t : X,
R : bin_rel X,
this : cls R t ∩ cls R s = ∅ ↔ ¬¬cls R t ∩ cls R s = ∅,
ha : ¬R s t,
hb : ¬cls R t ∩ cls R s = ∅,
x : X,
hα : x ∈ cls R t,
hβ : x ∈ cls R s,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R,
hc : R s x ∧ R x t,
hd : R s t
⊢ false
contradiction,
X : Type u,
s t : X,
R : bin_rel X,
this : cls R t ∩ cls R s = ∅ ↔ ¬¬cls R t ∩ cls R s = ∅,
ha : ¬R s t,
hb : ¬cls R t ∩ cls R s = ∅,
x : X,
hα : x ∈ cls R t,
hβ : x ∈ cls R s,
href : reflexive R,
hsym : symmetric R,
htrans : transitive R,
hc : R s x ∧ R x t,
hd : R s t
⊢ false
no goals
We now formally define a partition of a set $X$
Partition of a set $X$ is a set $A$ of non-empty subsets of $X$ with the property that each element of $X$ is in exacctly one of the subsets.
Theorem
Let $X$ be a set and let $R$ be an equivalence relation on $X$. Then the set $V$ of equivalence classes $\{cl(s) | s ∈ X\}$ for $R$ is a partition of $X$.
theorem equiv_relation_partition -- or replace the set with (set.range (cls R))
(R : bin_rel X) (h : equivalence R) : partition {a : set X | ∃ s : X, a = cls R s} :=
Proof
QED.
To show that the equivalence classes of $R$ form a partition of $X$, we need to show that every $x ∈ X$ is in exactly one equivalence class of $R$, AND, none of the equivalence classes are empty.
split,
X : Type u,
R : bin_rel X,
h : equivalence R
⊢ partition {a : set X | ∃ (s : X), a = cls R s}
2 goals
X : Type u,
R : bin_rel X,
h : equivalence R
⊢ ∀ (x : X),
∃ (B : set X) (H : B ∈ {a : set X | ∃ (s : X), a = cls R s}),
x ∈ B ∧ ∀ (C : set X), C ∈ {a : set X | ∃ (s : X), a = cls R s} → x ∈ C → B = C
X : Type u,
R : bin_rel X,
h : equivalence R
⊢ ∅ ∉ {a : set X | ∃ (s : X), a = cls R s}
So let's first show that every $x ∈ X$ is in exactly one equivalence class of $R$. Let $y$ be and element of $X$.
{simp, intro y,
2 goals
X : Type u,
R : bin_rel X,
h : equivalence R
⊢ ∀ (x : X),
∃ (B : set X) (H : B ∈ {a : set X | ∃ (s : X), a = cls R s}),
x ∈ B ∧ ∀ (C : set X), C ∈ {a : set X | ∃ (s : X), a = cls R s} → x ∈ C → B = C
X : Type u,
R : bin_rel X,
h : equivalence R
⊢ ∅ ∉ {a : set X | ∃ (s : X), a = cls R s}
X : Type u,
R : bin_rel X,
h : equivalence R,
y : X
⊢ ∃ (B : set X),
(∃ (s : X), B = cls R s) ∧ y ∈ B ∧ ∀ (C : set X) (x : X), C = cls R x → y ∈ C → B = C
existsi cls R y,
X : Type u,
R : bin_rel X,
h : equivalence R,
y : X
⊢ ∃ (B : set X),
(∃ (s : X), B = cls R s) ∧ y ∈ B ∧ ∀ (C : set X) (x : X), C = cls R x → y ∈ C → B = C
X : Type u,
R : bin_rel X,
h : equivalence R,
y : X
⊢ (∃ (s : X), cls R y = cls R s) ∧
y ∈ cls R y ∧ ∀ (C : set X) (x : X), C = cls R x → y ∈ C → cls R y = C
split,
X : Type u,
R : bin_rel X,
h : equivalence R,
y : X
⊢ (∃ (s : X), cls R y = cls R s) ∧
y ∈ cls R y ∧ ∀ (C : set X) (x : X), C = cls R x → y ∈ C → cls R y = C
2 goals
X : Type u,
R : bin_rel X,
h : equivalence R,
y : X
⊢ ∃ (s : X), cls R y = cls R s
X : Type u,
R : bin_rel X,
h : equivalence R,
y : X
⊢ y ∈ cls R y ∧ ∀ (C : set X) (x : X), C = cls R x → y ∈ C → cls R y = C
Then obviously $y ∈ cl(y)$ since $R(y, y)$ is true by reflexivity.
{use y},
2 goals
X : Type u,
R : bin_rel X,
h : equivalence R,
y : X
⊢ ∃ (s : X), cls R y = cls R s
X : Type u,
R : bin_rel X,
h : equivalence R,
y : X
⊢ y ∈ cls R y ∧ ∀ (C : set X) (x : X), C = cls R x → y ∈ C → cls R y = C
X : Type u,
R : bin_rel X,
h : equivalence R,
y : X
⊢ y ∈ cls R y ∧ ∀ (C : set X) (x : X), C = cls R x → y ∈ C → cls R y = C
{split,
X : Type u,
R : bin_rel X,
h : equivalence R,
y : X
⊢ y ∈ cls R y ∧ ∀ (C : set X) (x : X), C = cls R x → y ∈ C → cls R y = C
2 goals
X : Type u,
R : bin_rel X,
h : equivalence R,
y : X
⊢ y ∈ cls R y
X : Type u,
R : bin_rel X,
h : equivalence R,
y : X
⊢ ∀ (C : set X) (x : X), C = cls R x → y ∈ C → cls R y = C
{from itself_in_cls R h y},
2 goals
X : Type u,
R : bin_rel X,
h : equivalence R,
y : X
⊢ y ∈ cls R y
X : Type u,
R : bin_rel X,
h : equivalence R,
y : X
⊢ ∀ (C : set X) (x : X), C = cls R x → y ∈ C → cls R y = C
X : Type u,
R : bin_rel X,
h : equivalence R,
y : X
⊢ ∀ (C : set X) (x : X), C = cls R x → y ∈ C → cls R y = C
Okay. So now we need to prove uniqueness. Suppose there is a $x ∈ X$, $x ∈ cl(y)$, we then need to show $cl(y) = cl(x)$.
{intros C x hC hy_in_C, rw hC,
X : Type u,
R : bin_rel X,
h : equivalence R,
y : X
⊢ ∀ (C : set X) (x : X), C = cls R x → y ∈ C → cls R y = C
X : Type u,
R : bin_rel X,
h : equivalence R,
y : X,
C : set X,
x : X,
hC : C = cls R x,
hy_in_C : y ∈ C
⊢ cls R y = cls R x
But this is true by lemma (2)!
apply class_relate_lem_b, assumption,
X : Type u,
R : bin_rel X,
h : equivalence R,
y : X,
C : set X,
x : X,
hC : C = cls R x,
hy_in_C : y ∈ C
⊢ cls R y = cls R x
X : Type u,
R : bin_rel X,
h : equivalence R,
y : X,
C : set X,
x : X,
hC : C = cls R x,
hy_in_C : y ∈ C
⊢ R x y
have : y ∈ cls R x, rwa ←hC,
X : Type u,
R : bin_rel X,
h : equivalence R,
y : X,
C : set X,
x : X,
hC : C = cls R x,
hy_in_C : y ∈ C
⊢ R x y
X : Type u,
R : bin_rel X,
h : equivalence R,
y : X,
C : set X,
x : X,
hC : C = cls R x,
hy_in_C : y ∈ C,
this : y ∈ cls R x
⊢ R x y
unfold cls at this,
X : Type u,
R : bin_rel X,
h : equivalence R,
y : X,
C : set X,
x : X,
hC : C = cls R x,
hy_in_C : y ∈ C,
this : y ∈ cls R x
⊢ R x y
X : Type u,
R : bin_rel X,
h : equivalence R,
y : X,
C : set X,
x : X,
hC : C = cls R x,
hy_in_C : y ∈ C,
this : y ∈ {x_1 : X | R x x_1}
⊢ R x y
rwa set.mem_set_of_eq at this}
X : Type u,
R : bin_rel X,
h : equivalence R,
y : X,
C : set X,
x : X,
hC : C = cls R x,
hy_in_C : y ∈ C,
this : y ∈ {x_1 : X | R x x_1}
⊢ R x y
no goals
}
no goals
no goals
},
no goals
X : Type u,
R : bin_rel X,
h : equivalence R
⊢ ∅ ∉ {a : set X | ∃ (s : X), a = cls R s}
Now we have to prove that none of the equivalence classes are empty. But this is quite simple. Suppose there is an equivalence class $cl(x)$ where $x ∈ X$ that is empty.
{simp, intros x hx,
X : Type u,
R : bin_rel X,
h : equivalence R
⊢ ∅ ∉ {a : set X | ∃ (s : X), a = cls R s}
X : Type u,
R : bin_rel X,
h : equivalence R,
x : X,
hx : ∅ = cls R x
⊢ false
But then $x ∈ cl(x)$ as $R(x, x)$ is true by reflexivity. Ah ha! Contradiction! Hence, such empty equivalence class does not in fact exist! And we are done.
rw set.empty_def at hx,
X : Type u,
R : bin_rel X,
h : equivalence R,
x : X,
hx : ∅ = cls R x
⊢ false
X : Type u,
R : bin_rel X,
h : equivalence R,
x : X,
hx : {x : X | false} = cls R x
⊢ false
have : x ∈ {x : X | false}, by {rw hx, from itself_in_cls R h x},
X : Type u,
R : bin_rel X,
h : equivalence R,
x : X,
hx : {x : X | false} = cls R x
⊢ false
X : Type u,
R : bin_rel X,
h : equivalence R,
x : X,
hx : {x : X | false} = cls R x,
this : x ∈ {x : X | false}
⊢ false
rwa set.mem_set_of_eq at this
X : Type u,
R : bin_rel X,
h : equivalence R,
x : X,
hx : {x : X | false} = cls R x,
this : x ∈ {x : X | false}
⊢ false
X : Type u,
R : bin_rel X,
h : equivalence R,
x : X,
hx : {x : X | false} = cls R x,
this : x ∈ {x : X | false}
⊢ false
}
X : Type u,
R : bin_rel X,
h : equivalence R,
x : X,
hx : {x : X | false} = cls R x,
this : x ∈ {x : X | false}
⊢ false
no goals
Bonus Exercise. Furthermore, it turns out that if $X$ is a set and $R$ an equivalence relation on $X$. Then any partition of $X$ can form a equivalence relation. Try to prove it here and if you get stuck, here are the solutions.