Functions
2.2.1 Function Composition
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
def my_injective {X Y : Type u} (f : X → Y) := ∀ a b : X, f(a) = f(b) → a = b
def my_surjective {X Y : Type u} (f : X → Y) := ∀ y : Y, ∃ x : X, f(x) = y
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
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) :=
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
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
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!
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) :=
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
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
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
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
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) :=
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)
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)
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
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
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)
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 :=
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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
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
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
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
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
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
def bin_rel (X) := X → X → Prop
2.6 Common Predicates on Binary Relations
def reflexive (r : bin_rel X) := ∀ x : X, r x x
$≤$ is reflexive on $ℝ$.
@[simp] theorem le_refl : reflexive ((≤) : ℝ → ℝ → Prop) :=
intro,
⊢ reflexive has_le.le
x : ℝ
⊢ x ≤ x
refl
x : ℝ
⊢ x ≤ x
x : ℝ
⊢ x ≤ x
def symmetric (r : bin_rel X) := ∀ x y : X, r x y → r y x
$=$ is symmetric on $ℝ$.
theorem eq_symm : symmetric ((=) : ℝ → ℝ → Prop) :=
intros x y h,
⊢ symmetric eq
x y : ℝ,
h : x = y
⊢ y = x
rwa h
x y : ℝ,
h : x = y
⊢ y = x
x y : ℝ,
h : x = y
⊢ y = x
def antisymmetric (r : bin_rel X) := ∀ x y : X, r x y ∧ r y x → x = y
$≤$ is anti-symmetric on $R$.
@[simp] theorem le_antisymm : antisymmetric ((≤) : ℝ → ℝ → Prop) :=
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
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
{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
{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
{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.
def transitive (r : bin_rel X) := ∀ x y z : X, r x y ∧ r y z → r x z
$⇒$ is transitive on the set of propositions.
theorem imply_trans : transitive ((→) : Prop → Prop → Prop) :=
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
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
$≤$ is transitive on $ℝ$.
@[simp] theorem le_trans : transitive ((≤) : ℝ → ℝ → Prop) :=
intros x y z h,
⊢ transitive has_le.le
x y z : ℝ,
h : x ≤ y ∧ y ≤ z
⊢ x ≤ z
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$.
def partial_order (r : bin_rel X) := reflexive r ∧ antisymmetric r ∧ transitive r
def total (r : bin_rel X) := ∀ x y : X, r x y ∨ r y x
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.
$≤$ is total on $ℝ$.
@[simp] theorem le_total : total ((≤) : ℝ → ℝ → Prop) :=
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
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
{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.
$≤$ is a total order on $ℝ$.
theorem le_total_order : total_order ((≤) : ℝ → ℝ → Prop) :=
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
def equivalence (r : bin_rel X) := reflexive r ∧ symmetric r ∧ transitive r
We'll present some examples of equivalence relations below.
def R (m n : ℤ) := 2 ∣ (m - n)
(1) $R$ is reflexive.
lemma R_refl : reflexive R :=
intro,
⊢ reflexive R
x : ℤ
⊢ R x x
unfold R,
x : ℤ
⊢ R x x
x : ℤ
⊢ 2 ∣ x - x
simp,
x : ℤ
⊢ 2 ∣ x - x
no goals
(2) $R$ is symmetric.
lemma R_symm : symmetric R :=
intros m n,
⊢ symmetric R
m n : ℤ
⊢ R m n → R n m
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
simp, rw ←hx, ring,
m n x : ℤ,
hx : m - n = 2 * x
⊢ n - m = 2 * -x
no goals
(3) $R$ is transitive.
lemma R_trans : transitive R :=
intros l m n,
⊢ transitive R
l m n : ℤ
⊢ R l m ∧ R m n → R 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)
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
$R$ is an equivalence relation.
theorem R_equiv : equivalence R :=
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
def brel (A B : Type*) := ∃ g : A → B, function.bijective g
infix ` <~ `: 50 := brel
$<\mathtt{\sim}$ is reflexive.
@[simp] lemma brel_refl : reflexive (<~) :=
intro X,
⊢ reflexive brel
X : Type u_1
⊢ X <~ X
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
from function.bijective_id
X : Type u_1,
g : X → X := id
⊢ bijective g
X : Type u_1,
g : X → X := id
⊢ bijective g
$<\mathtt{\sim}$ is symmetric.
@[simp] lemma brel_symm : symmetric (<~) :=
intros X Y,
⊢ symmetric brel
X Y : Type u_1
⊢ X <~ Y → Y <~ X
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
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
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
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
$<\mathtt{\sim}$ is transitive.
@[simp] lemma brel_trans : transitive (<~) :=
intros X Y Z,
⊢ transitive brel
X Y Z : Type u_1
⊢ X <~ Y ∧ Y <~ Z → X <~ 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
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!
$<\mathtt{\sim}$ is an equivalence relation
theorem brel_equiv : equivalence (<~) :=
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
def cls (r : bin_rel X) (s : X) := {x : X | r s x}
(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 :=
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
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
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)$.
(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 :=
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
{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
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
(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 = ∅ :=
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
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
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
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.
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} :=
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}
{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
{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
{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
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}
{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
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.