5. Projects
Summary: In the second phase of this course, students can assign themselves projects. For this, they were asked to look for simple exercises, e.g. from their first year courses. Here comes a list of exercises they used.
5.1. Induction (Luis Jaschke und Felicitas Kissel)
Compute the following sums and products, and show your result by induction.
open Finset
example (n : ℕ) :
∑ k ∈ range (n + 1), (k:ℝ) ^ 2 =
n * (n + 1) * (2*n + 1) / 6 := n:ℕ⊢ ∑ k ∈ range (n + 1), ↑k ^ 2 = ↑n * (↑n + 1) * (2 * ↑n + 1) / 6
induction n with
| zero => All goals completed! 🐙
| succ n ih =>
n:ℕih:∑ k ∈ range (n + 1), ↑k ^ 2 = ↑n * (↑n + 1) * (2 * ↑n + 1) / 6⊢ ∑ x ∈ range (n + 1), ↑x ^ 2 + ↑(n + 1) ^ 2 = ↑(n + 1) * (↑(n + 1) + 1) * (2 * ↑(n + 1) + 1) / 6
n:ℕih:∑ k ∈ range (n + 1), ↑k ^ 2 = ↑n * (↑n + 1) * (2 * ↑n + 1) / 6⊢ ↑n * (↑n + 1) * (2 * ↑n + 1) / 6 + ↑(n + 1) ^ 2 = ↑(n + 1) * (↑(n + 1) + 1) * (2 * ↑(n + 1) + 1) / 6
n:ℕih:∑ k ∈ range (n + 1), ↑k ^ 2 = ↑n * (↑n + 1) * (2 * ↑n + 1) / 6⊢ ↑n * (1 / 6) + ↑n ^ 2 * (1 / 2) + ↑n ^ 3 * (1 / 3) + ↑(1 + n) ^ 2 =
↑(1 + n) * (1 / 6) + ↑(1 + n) ^ 2 * (1 / 2) + ↑(1 + n) ^ 3 * (1 / 3)
n:ℕih:∑ k ∈ range (n + 1), ↑k ^ 2 = ↑n * (↑n + 1) * (2 * ↑n + 1) / 6⊢ (↑n * 2 + ↑n ^ 2 * 6) * 3 + ↑n ^ 3 * (6 * 2) + (1 + ↑n) ^ 2 * (6 * 2 * 3) =
((1 + ↑n) * 2 + (1 + ↑n) ^ 2 * 6) * 3 + (1 + ↑n) ^ 3 * (6 * 2)
All goals completed! 🐙
example (n : ℕ) :
∑ k ∈ Finset.range (n + 1), (k : ℝ) ^ 3 =
n * n * (n + 1) * (n + 1) / 4 := n:ℕ⊢ ∑ k ∈ range (n + 1), ↑k ^ 3 = ↑n * ↑n * (↑n + 1) * (↑n + 1) / 4
induction n with
| zero => All goals completed! 🐙
| succ n ih =>
n:ℕih:∑ k ∈ range (n + 1), ↑k ^ 3 = ↑n * ↑n * (↑n + 1) * (↑n + 1) / 4⊢ ↑n * ↑n * (↑n + 1) * (↑n + 1) / 4 + ↑(n + 1) ^ 3 = ↑(n + 1) * ↑(n + 1) * (↑(n + 1) + 1) * (↑(n + 1) + 1) / 4
n:ℕih:∑ k ∈ range (n + 1), ↑k ^ 3 = ↑n * ↑n * (↑n + 1) * (↑n + 1) / 4⊢ ↑n ^ 2 * (1 / 4) + ↑n ^ 3 * (1 / 2) + ↑n ^ 4 * (1 / 4) + ↑(1 + n) ^ 3 =
↑(1 + n) ^ 2 * (1 / 4) + ↑(1 + n) ^ 3 * (1 / 2) + ↑(1 + n) ^ 4 * (1 / 4)
n:ℕih:∑ k ∈ range (n + 1), ↑k ^ 3 = ↑n * ↑n * (↑n + 1) * (↑n + 1) / 4⊢ (↑n ^ 2 * 2 + ↑n ^ 3 * 4) * 4 + ↑n ^ 4 * (4 * 2) + (1 + ↑n) ^ 3 * (4 * 2 * 4) =
((1 + ↑n) ^ 2 * 2 + (1 + ↑n) ^ 3 * 4) * 4 + (1 + ↑n) ^ 4 * (4 * 2)
All goals completed! 🐙
example (n : ℕ) :
∑ k ∈ Finset.range n, (2 * (k : ℝ) + 1) = (n : ℝ)^2 := n:ℕ⊢ ∑ k ∈ range n, (2 * ↑k + 1) = ↑n ^ 2
induction n with
| zero =>
All goals completed! 🐙
| succ n ih =>
n:ℕih:∑ k ∈ range n, (2 * ↑k + 1) = ↑n ^ 2⊢ ↑n ^ 2 + (2 * ↑n + 1) = ↑(n + 1) ^ 2
n:ℕih:∑ k ∈ range n, (2 * ↑k + 1) = ↑n ^ 2⊢ ↑n ^ 2 + (2 * ↑n + 1) = (↑n + 1) ^ 2
All goals completed! 🐙
open Finset
example (n : ℕ) :
∏ k ∈ Finset.range n, (1 + 1 / (k + 1 : ℚ)) = n + 1
:= n:ℕ⊢ ∏ k ∈ range n, (1 + 1 / (↑k + 1)) = ↑n + 1
-- gleicher Nenner: 1 + (1/(k+1)) = (1+2)/(k+1)
have h_gleicher_Nenner :
∏ k ∈ Finset.range n, (1 + 1 / (k + 1 : ℚ)) =
∏ k ∈ Finset.range n, ((k + 2) : ℚ) / (k + 1)
:= n:ℕ⊢ ∏ k ∈ range n, (1 + 1 / (↑k + 1)) = ↑n + 1
n:ℕ⊢ ∀ x ∈ range n, 1 + 1 / (↑x + 1) = (↑x + 2) / (↑x + 1)
n:ℕk:ℕhk:k ∈ range n⊢ 1 + 1 / (↑k + 1) = (↑k + 2) / (↑k + 1)
n:ℕk:ℕhk:k ∈ range n⊢ ↑k + 1 + 1 = ↑k + 2
All goals completed! 🐙
n:ℕh_gleicher_Nenner:∏ k ∈ range n, (1 + 1 / (↑k + 1)) = ∏ k ∈ range n, (↑k + 2) / (↑k + 1)⊢ ∏ k ∈ range n, (↑k + 2) / (↑k + 1) = ↑n + 1
-- Nun zur Induktion
induction n with
| zero => All goals completed! 🐙
| succ n kh =>
n:ℕkh:∏ k ∈ range n, (1 + 1 / (↑k + 1)) = ∏ k ∈ range n, (↑k + 2) / (↑k + 1) → ∏ k ∈ range n, (↑k + 2) / (↑k + 1) = ↑n + 1h_gleicher_Nenner:∏ k ∈ range (n + 1), (1 + 1 / (↑k + 1)) = ∏ k ∈ range (n + 1), (↑k + 2) / (↑k + 1)⊢ (↑n + 2) / (↑n + 1) * ∏ x ∈ range n, (↑x + 2) / (↑x + 1) = ↑(n + 1) + 1
have h' := kh (n:ℕkh:∏ k ∈ range n, (1 + 1 / (↑k + 1)) = ∏ k ∈ range n, (↑k + 2) / (↑k + 1) → ∏ k ∈ range n, (↑k + 2) / (↑k + 1) = ↑n + 1h_gleicher_Nenner:∏ k ∈ range (n + 1), (1 + 1 / (↑k + 1)) = ∏ k ∈ range (n + 1), (↑k + 2) / (↑k + 1)⊢ ∏ k ∈ range n, (1 + 1 / (↑k + 1)) = ∏ k ∈ range n, (↑k + 2) / (↑k + 1)
n:ℕkh:∏ k ∈ range n, (1 + 1 / (↑k + 1)) = ∏ k ∈ range n, (↑k + 2) / (↑k + 1) → ∏ k ∈ range n, (↑k + 2) / (↑k + 1) = ↑n + 1h_gleicher_Nenner:∏ k ∈ range (n + 1), (1 + 1 / (↑k + 1)) = ∏ k ∈ range (n + 1), (↑k + 2) / (↑k + 1)⊢ ∀ x ∈ range n, 1 + 1 / (↑x + 1) = (↑x + 2) / (↑x + 1)
n:ℕkh:∏ k ∈ range n, (1 + 1 / (↑k + 1)) = ∏ k ∈ range n, (↑k + 2) / (↑k + 1) → ∏ k ∈ range n, (↑k + 2) / (↑k + 1) = ↑n + 1h_gleicher_Nenner:∏ k ∈ range (n + 1), (1 + 1 / (↑k + 1)) = ∏ k ∈ range (n + 1), (↑k + 2) / (↑k + 1)k:ℕhk:k ∈ range n⊢ 1 + 1 / (↑k + 1) = (↑k + 2) / (↑k + 1)
n:ℕkh:∏ k ∈ range n, (1 + 1 / (↑k + 1)) = ∏ k ∈ range n, (↑k + 2) / (↑k + 1) → ∏ k ∈ range n, (↑k + 2) / (↑k + 1) = ↑n + 1h_gleicher_Nenner:∏ k ∈ range (n + 1), (1 + 1 / (↑k + 1)) = ∏ k ∈ range (n + 1), (↑k + 2) / (↑k + 1)k:ℕhk:k ∈ range n⊢ ↑k + 1 + 1 = ↑k + 2
All goals completed! 🐙)
n:ℕkh:∏ k ∈ range n, (1 + 1 / (↑k + 1)) = ∏ k ∈ range n, (↑k + 2) / (↑k + 1) → ∏ k ∈ range n, (↑k + 2) / (↑k + 1) = ↑n + 1h_gleicher_Nenner:∏ k ∈ range (n + 1), (1 + 1 / (↑k + 1)) = ∏ k ∈ range (n + 1), (↑k + 2) / (↑k + 1)h':∏ k ∈ range n, (↑k + 2) / (↑k + 1) = ↑n + 1⊢ (↑n + 2) / (↑n + 1) * (↑n + 1) = ↑(n + 1) + 1
n:ℕkh:∏ k ∈ range n, (1 + 1 / (↑k + 1)) = ∏ k ∈ range n, (↑k + 2) / (↑k + 1) → ∏ k ∈ range n, (↑k + 2) / (↑k + 1) = ↑n + 1h_gleicher_Nenner:∏ k ∈ range (n + 1), (1 + 1 / (↑k + 1)) = ∏ k ∈ range (n + 1), (↑k + 2) / (↑k + 1)h':∏ k ∈ range n, (↑k + 2) / (↑k + 1) = ↑n + 1⊢ ↑n + 2 = ↑n + 1 + 1
All goals completed! 🐙
example (q : ℝ) (hq : abs q < 1) :
Filter.Tendsto (fun n ↦ q^n) atTop (nhds 0) := atTop:Filter ℕq:ℝhq:|q| < 1⊢ Filter.Tendsto (fun n => q ^ n) atTop (nhds 0)
All goals completed! 🐙
5.2. Own addition on ℚ (Adrian Eckstein und Debora Ortlieb)
open Rat
open BigOperators
-- Zu bearbeiten war das `Blatt 1` der Vorlesung `Lineare Algebra I` im _WiSe 2021/22_
-- an der _Universität Freiburg_ bei _Prof. Dr. Heike Mildenberger_.
-- `Aufgabe 1`: Betrachten Sie auf der Menge der rationalen Zahlen ℚ die folgende Verknüpfung.
-- Definiere die Operation _star_: a ∗ b := ab + 2a + 2b + 2
def star (a b : ℚ) : ℚ
:= a * b + 2 * a + 2 * b + 2
theorem LA1_Sheet1_Task1a (a b : ℚ) : star a b = star b a := a:ℚb:ℚ⊢ _root_.star a b = _root_.star b a
a:ℚb:ℚ⊢ a * b + 2 * a + 2 * b + 2 = b * a + 2 * b + 2 * a + 2
All goals completed! 🐙
-- `Aufgabe 1b`: Ist _(ℚ, star)_ assoziativ?
-- Beweis der Assoziativität: (a ∗ b) ∗ c = a ∗ (b ∗ c)
theorem LA1_Sheet1_Task1b (a b c : ℚ) :
star (star a b) c = star a (star b c)
:= a:ℚb:ℚc:ℚ⊢ _root_.star (_root_.star a b) c = _root_.star a (_root_.star b c)
a:ℚb:ℚc:ℚ⊢ (a * b + 2 * a + 2 * b + 2) * c + 2 * (a * b + 2 * a + 2 * b + 2) + 2 * c + 2 =
a * (b * c + 2 * b + 2 * c + 2) + 2 * a + 2 * (b * c + 2 * b + 2 * c + 2) + 2
All goals completed! 🐙
-- `Aufgabe 1c`: Besitzt _(ℚ, star)_ ein neutrales Element?
-- Beweis: -1 ist das neutrale Element, d.h. -1 ∗ a = a und a ∗ (-1) = a
theorem LA1_Sheet1_Task1c (a : ℚ) :
star (-1) a = a ∧ star a (-1) = a
:= a:ℚ⊢ _root_.star (-1) a = a ∧ _root_.star a (-1) = a
a:ℚ⊢ -1 * a + 2 * -1 + 2 * a + 2 = a ∧ a * -1 + 2 * a + 2 * -1 + 2 = a
a:ℚ⊢ -1 * a + 2 * -1 + 2 * a + 2 = aa:ℚ⊢ a * -1 + 2 * a + 2 * -1 + 2 = a
a:ℚ⊢ -1 * a + 2 * -1 + 2 * a + 2 = a All goals completed! 🐙
a:ℚ⊢ a * -1 + 2 * a + 2 * -1 + 2 = a All goals completed! 🐙
-- `Aufgabe 1d`: Ist _(ℚ, star)_ eine Gruppe?
-- Zeige: Nein, da -2 kein Inverses bezüglich _star_ hat.
theorem LA1_Sheet1_Task1d : ¬ ∃ b : ℚ, star (-2) b = -1
:= ⊢ ¬∃ b, _root_.star (-2) b = -1
h:∃ b, _root_.star (-2) b = -1⊢ False
b:ℚhb:_root_.star (-2) b = -1⊢ False
b:ℚhb:-2 * b + 2 * -2 + 2 * b + 2 = -1⊢ False
b:ℚhb:-2 = -1⊢ False
All goals completed! 🐙
theorem Ana1_Sheet1_Task3d (n : ℕ) (hn : 1 < n) :
∏ i ∈ Finset.range n, (1 - 1 / (i + 1 : ℚ)) = 0
:= n:ℕhn:1 < n⊢ ∏ i ∈ range n, (1 - 1 / (↑i + 1)) = 0
have h_mem : 0 ∈ Finset.range n
:= n:ℕhn:1 < n⊢ ∏ i ∈ range n, (1 - 1 / (↑i + 1)) = 0
n:ℕhn:1 < nh_pos:0 < n⊢ 0 ∈ range n
All goals completed! 🐙
n:ℕhn:1 < nh_mem:0 ∈ range n⊢ 1 - 1 / (↑0 + 1) = 0
All goals completed! 🐙
5.3. Path-connected spaces (Jasper Ganten)
open Set
section PathConnected
variable {X : Type*} [TopologicalSpace X]
/--
An intuitive definition of path connectedness:
A set `S` is path connected if it is nonempty and any two
points in `S` can be joined by a continuous path in `S`.
-/
def IsPathConnected' (S : Set X) : Prop :=
S.Nonempty ∧
∀ x y : X, x ∈ S → y ∈ S →
∃ γ : Set.Icc (0 : ℝ) 1 → X,
Continuous γ ∧
γ 0 = x ∧
γ 1 = y ∧
∀ t, γ t ∈ S
/--
`IsPathConnected'` is equivalent to Mathlib's
`IsPathConnected`.
-/
theorem pathConnected_iff (A : Set X) :
IsPathConnected A ↔ IsPathConnected' A := X:Type u_1inst✝:TopologicalSpace XA:Set X⊢ IsPathConnected A ↔ IsPathConnected' A
X:Type u_1inst✝:TopologicalSpace XA:Set X⊢ IsPathConnected A → IsPathConnected' AX:Type u_1inst✝:TopologicalSpace XA:Set X⊢ IsPathConnected' A → IsPathConnected A
X:Type u_1inst✝:TopologicalSpace XA:Set X⊢ IsPathConnected A → IsPathConnected' A -- Mathlib ⇒ Intuitive
X:Type u_1inst✝:TopologicalSpace XA:Set Xp1:Xhp1:p1 ∈ Ah1:∀ {y : X}, y ∈ A → JoinedIn A p1 y⊢ IsPathConnected' A
-- show that the set is nonempty
X:Type u_1inst✝:TopologicalSpace XA:Set Xp1:Xhp1:p1 ∈ Ah1:∀ {y : X}, y ∈ A → JoinedIn A p1 y⊢ ∀ (x y : X), x ∈ A → y ∈ A → ∃ γ, Continuous γ ∧ γ 0 = x ∧ γ 1 = y ∧ ∀ (t : ↑(Set.Icc 0 1)), γ t ∈ A
X:Type u_1inst✝:TopologicalSpace XA:Set Xp1:Xhp1:p1 ∈ Ah1:∀ {y : X}, y ∈ A → JoinedIn A p1 yp2:Xp3:Xhp2:p2 ∈ Ahp3:p3 ∈ A⊢ ∃ γ, Continuous γ ∧ γ 0 = p2 ∧ γ 1 = p3 ∧ ∀ (t : ↑(Set.Icc 0 1)), γ t ∈ A
-- construct a path from p2 to p3 by using the
-- transitivity of the JoinedIn relation
X:Type u_1inst✝:TopologicalSpace XA:Set Xp1:Xhp1:p1 ∈ Ah1:∀ {y : X}, y ∈ A → JoinedIn A p1 yp2:Xp3:Xhp2:p2 ∈ Ahp3:p3 ∈ Aγ:_root_.Path p2 p3hγ:∀ (t : ↑unitInterval), γ t ∈ A⊢ ∃ γ, Continuous γ ∧ γ 0 = p2 ∧ γ 1 = p3 ∧ ∀ (t : ↑(Set.Icc 0 1)), γ t ∈ A
All goals completed! 🐙
X:Type u_1inst✝:TopologicalSpace XA:Set X⊢ IsPathConnected' A → IsPathConnected A -- Intuitive ⇒ Mathlib
X:Type u_1inst✝:TopologicalSpace XA:Set Xhne:A.NonemptyhC:∀ (x y : X), x ∈ A → y ∈ A → ∃ γ, Continuous γ ∧ γ 0 = x ∧ γ 1 = y ∧ ∀ (t : ↑(Set.Icc 0 1)), γ t ∈ A⊢ IsPathConnected A
X:Type u_1inst✝:TopologicalSpace XA:Set XhC:∀ (x y : X), x ∈ A → y ∈ A → ∃ γ, Continuous γ ∧ γ 0 = x ∧ γ 1 = y ∧ ∀ (t : ↑(Set.Icc 0 1)), γ t ∈ Ax:Xhx:x ∈ A⊢ IsPathConnected A
X:Type u_1inst✝:TopologicalSpace XA:Set XhC:∀ (x y : X), x ∈ A → y ∈ A → ∃ γ, Continuous γ ∧ γ 0 = x ∧ γ 1 = y ∧ ∀ (t : ↑(Set.Icc 0 1)), γ t ∈ Ax:Xhx:x ∈ Ay:Xhy:y ∈ A⊢ JoinedIn A x y
X:Type u_1inst✝:TopologicalSpace XA:Set XhC:∀ (x y : X), x ∈ A → y ∈ A → ∃ γ, Continuous γ ∧ γ 0 = x ∧ γ 1 = y ∧ ∀ (t : ↑(Set.Icc 0 1)), γ t ∈ Ax:Xhx:x ∈ Ay:Xhy:y ∈ Aγ:↑(Set.Icc 0 1) → Xγ_cont:Continuous γγ0:γ 0 = xγ1:γ 1 = yhγ:∀ (t : ↑(Set.Icc 0 1)), γ t ∈ A⊢ JoinedIn A x y
-- construct a Path type from my intuitive definition
X:Type u_1inst✝:TopologicalSpace XA:Set XhC:∀ (x y : X), x ∈ A → y ∈ A → ∃ γ, Continuous γ ∧ γ 0 = x ∧ γ 1 = y ∧ ∀ (t : ↑(Set.Icc 0 1)), γ t ∈ Ax:Xhx:x ∈ Ay:Xhy:y ∈ Aγ:↑(Set.Icc 0 1) → Xγ_cont:Continuous γγ0:γ 0 = xγ1:γ 1 = yhγ:∀ (t : ↑(Set.Icc 0 1)), γ t ∈ Ap:_root_.Path x y := { toFun := γ, continuous_toFun := γ_cont, source' := γ0, target' := γ1 }⊢ JoinedIn A x y
All goals completed! 🐙
/--
If `A` and `B` are path connected, and their intersetion
is nonempty, `A ∪ B` is pathconnected.
-/
theorem my_task {A B : Set X} (hA : IsPathConnected A)
(hB : IsPathConnected B) (hAB : (A ∩ B).Nonempty) :
IsPathConnected (A ∪ B) := X:Type u_1inst✝:TopologicalSpace XA:Set XB:Set XhA:IsPathConnected AhB:IsPathConnected BhAB:(A ∩ B).Nonempty⊢ IsPathConnected (A ∪ B)
-- select a point z in the intersection
X:Type u_1inst✝:TopologicalSpace XA:Set XB:Set XhA:IsPathConnected AhB:IsPathConnected Bx:XhxA:x ∈ AhxB:x ∈ B⊢ IsPathConnected (A ∪ B)
X:Type u_1inst✝:TopologicalSpace XA:Set XB:Set XhA:IsPathConnected AhB:IsPathConnected Bx:XhxA:x ∈ AhxB:x ∈ B⊢ x ∈ A ∪ B ∧ ∀ {y : X}, y ∈ A ∪ B → JoinedIn (A ∪ B) x y
X:Type u_1inst✝:TopologicalSpace XA:Set XB:Set XhA:IsPathConnected AhB:IsPathConnected Bx:XhxA:x ∈ AhxB:x ∈ By:Xhy:y ∈ A ∪ B⊢ JoinedIn (A ∪ B) x y
-- split in cases depending on where y is
X:Type u_1inst✝:TopologicalSpace XA:Set XB:Set XhA:IsPathConnected AhB:IsPathConnected Bx:XhxA:x ∈ AhxB:x ∈ By:XhyA:y ∈ A⊢ JoinedIn (A ∪ B) x yX:Type u_1inst✝:TopologicalSpace XA:Set XB:Set XhA:IsPathConnected AhB:IsPathConnected Bx:XhxA:x ∈ AhxB:x ∈ By:XhyB:y ∈ B⊢ JoinedIn (A ∪ B) x y
X:Type u_1inst✝:TopologicalSpace XA:Set XB:Set XhA:IsPathConnected AhB:IsPathConnected Bx:XhxA:x ∈ AhxB:x ∈ By:XhyA:y ∈ A⊢ JoinedIn (A ∪ B) x y -- y ∈ A then x and y are joined in A
X:Type u_1inst✝:TopologicalSpace XA:Set XB:Set XhA:IsPathConnected AhB:IsPathConnected Bx:XhxA:x ∈ AhxB:x ∈ By:XhyA:y ∈ AjoinedInA:JoinedIn A x y⊢ JoinedIn (A ∪ B) x y
-- but then also in the superset A ∪ B
All goals completed! 🐙
X:Type u_1inst✝:TopologicalSpace XA:Set XB:Set XhA:IsPathConnected AhB:IsPathConnected Bx:XhxA:x ∈ AhxB:x ∈ By:XhyB:y ∈ B⊢ JoinedIn (A ∪ B) x y -- y ∈ A then x and y are joined in B
X:Type u_1inst✝:TopologicalSpace XA:Set XB:Set XhA:IsPathConnected AhB:IsPathConnected Bx:XhxA:x ∈ AhxB:x ∈ By:XhyB:y ∈ BjoinedInB:JoinedIn B x y⊢ JoinedIn (A ∪ B) x y
-- but then also in the superset A ∪ B
All goals completed! 🐙
end PathConnected
5.4. A homomorphism is injective iff its kernel is trivial (Moritz Graßnitzer, Natalie Jahnes)
structure our_Group where
uni : Type
mul : uni → uni → uni
one : uni
inv : uni → uni
mul_assoc : ∀ a b c : uni, mul (mul a b) c = mul a (mul b c)
one_mul : ∀ a : uni, mul one a = a
mul_one : ∀ a : uni, mul a one = a
mul_inv : ∀ a : uni, mul a (inv a) = one
inv_mul : ∀ a : uni, mul (inv a) a = one
lemma our_unique_inv {G : our_Group} (a b : G.uni) : G.mul a b = G.one → b = G.inv a := G:our_Groupa:G.unib:G.uni⊢ G.mul a b = G.one → b = G.inv a
G:our_Groupa:G.unib:G.unih:G.mul a b = G.one⊢ b = G.inv a
G:our_Groupa:G.unib:G.unih:G.mul a b = G.oneh1:G.mul a (G.inv a) = G.one⊢ b = G.inv a
G:our_Groupa:G.unib:G.unih:G.mul a b = G.oneh1:G.mul a (G.inv a) = G.mul a b⊢ b = G.inv a
have h2 : G.mul (G.inv a) (G.mul a b) = G.mul (G.inv a) G.one := G:our_Groupa:G.unib:G.uni⊢ G.mul a b = G.one → b = G.inv a All goals completed! 🐙
have h3 : G.mul (G.mul (G.inv a) a) b = G.mul (G.inv a) G.one := G:our_Groupa:G.unib:G.uni⊢ G.mul a b = G.one → b = G.inv a All goals completed! 🐙
have h4 : G.mul (G.one) b = G.mul (G.inv a) G.one := G:our_Groupa:G.unib:G.uni⊢ G.mul a b = G.one → b = G.inv a
G:our_Groupa:G.unib:G.unih:G.mul a b = G.oneh1:G.mul a (G.inv a) = G.mul a bh2:G.mul (G.inv a) (G.mul a b) = G.mul (G.inv a) G.oneh3:G.mul G.one b = G.mul (G.inv a) G.one⊢ G.mul G.one b = G.mul (G.inv a) G.one
All goals completed! 🐙
have h5 : b = G.mul (G.inv a) G.one := G:our_Groupa:G.unib:G.uni⊢ G.mul a b = G.one → b = G.inv a
G:our_Groupa:G.unib:G.unih:G.mul a b = G.oneh1:G.mul a (G.inv a) = G.mul a bh2:G.mul (G.inv a) (G.mul a b) = G.mul (G.inv a) G.oneh3:G.mul (G.mul (G.inv a) a) b = G.mul (G.inv a) G.oneh4:b = G.mul (G.inv a) G.one⊢ b = G.mul (G.inv a) G.one
All goals completed! 🐙
have h6 : b = G.inv a := G:our_Groupa:G.unib:G.uni⊢ G.mul a b = G.one → b = G.inv a
G:our_Groupa:G.unib:G.unih:G.mul a b = G.oneh1:G.mul a (G.inv a) = G.mul a bh2:G.mul (G.inv a) (G.mul a b) = G.mul (G.inv a) G.oneh3:G.mul (G.mul (G.inv a) a) b = G.mul (G.inv a) G.oneh4:G.mul G.one b = G.mul (G.inv a) G.oneh5:b = G.inv a⊢ b = G.inv a
All goals completed! 🐙
All goals completed! 🐙
lemma our_unique_inv_inv {G : our_Group} (a : G.uni) : a = G.inv (G.inv a) := G:our_Groupa:G.uni⊢ a = G.inv (G.inv a)
G:our_Groupa:G.unih1:G.mul (G.inv a) a = G.one⊢ a = G.inv (G.inv a)
G:our_Groupa:G.unih1:a = G.inv (G.inv a)⊢ a = G.inv (G.inv a)
All goals completed! 🐙
5.5. There is only one prime triplet (Patrick Nasdala, Max Lehr)
There is only one prime triplet, i.e. only one n : ℕ
prime, such that n + 2
and n + 4
are prime as well.
lemma div3 (n : ℕ) : (3 ∣ n) ∨ (3 ∣ (n+1)) ∨ (3 ∣ (n+2)) := n:ℕ⊢ 3 ∣ n ∨ 3 ∣ n + 1 ∨ 3 ∣ n + 2
induction n with
| zero =>
⊢ 3 ∣ 0
All goals completed! 🐙
| succ n hn =>
n:ℕhn:3 ∣ n ∨ 3 ∣ n + 1 ∨ 3 ∣ n + 2⊢ 3 ∣ 1 + n ∨ 3 ∣ 2 + n ∨ 3 ∣ 3 + n
n:ℕhn:3 ∣ n ∨ 3 ∣ n + 1 ∨ 3 ∣ n + 2h0:3 ∣ n⊢ 3 ∣ 1 + n ∨ 3 ∣ 2 + n ∨ 3 ∣ 3 + nn:ℕhn:3 ∣ n ∨ 3 ∣ n + 1 ∨ 3 ∣ n + 2h0:¬3 ∣ n⊢ 3 ∣ 1 + n ∨ 3 ∣ 2 + n ∨ 3 ∣ 3 + n
n:ℕhn:3 ∣ n ∨ 3 ∣ n + 1 ∨ 3 ∣ n + 2h0:3 ∣ n⊢ 3 ∣ 1 + n ∨ 3 ∣ 2 + n ∨ 3 ∣ 3 + n n:ℕhn:3 ∣ n ∨ 3 ∣ n + 1 ∨ 3 ∣ n + 2h0:3 ∣ n⊢ 3 ∣ 2 + n ∨ 3 ∣ 3 + n
n:ℕhn:3 ∣ n ∨ 3 ∣ n + 1 ∨ 3 ∣ n + 2h0:3 ∣ n⊢ 3 ∣ 3 + n
All goals completed! 🐙
n:ℕhn:3 ∣ n ∨ 3 ∣ n + 1 ∨ 3 ∣ n + 2h0:¬3 ∣ n⊢ 3 ∣ 1 + n ∨ 3 ∣ 2 + n ∨ 3 ∣ 3 + n n:ℕhn:3 ∣ n ∨ 3 ∣ n + 1 ∨ 3 ∣ n + 2h0:¬3 ∣ nh1:3 ∣ n + 1⊢ 3 ∣ 1 + n ∨ 3 ∣ 2 + n ∨ 3 ∣ 3 + nn:ℕhn:3 ∣ n ∨ 3 ∣ n + 1 ∨ 3 ∣ n + 2h0:¬3 ∣ nh1:¬3 ∣ n + 1⊢ 3 ∣ 1 + n ∨ 3 ∣ 2 + n ∨ 3 ∣ 3 + n
n:ℕhn:3 ∣ n ∨ 3 ∣ n + 1 ∨ 3 ∣ n + 2h0:¬3 ∣ nh1:3 ∣ n + 1⊢ 3 ∣ 1 + n ∨ 3 ∣ 2 + n ∨ 3 ∣ 3 + n n:ℕhn:3 ∣ n ∨ 3 ∣ n + 1 ∨ 3 ∣ n + 2h0:¬3 ∣ nh1:3 ∣ n + 1⊢ 3 ∣ 1 + n
n:ℕhn:3 ∣ n ∨ 3 ∣ n + 1 ∨ 3 ∣ n + 2h0:¬3 ∣ nh1:3 ∣ 1 + n⊢ 3 ∣ 1 + n
All goals completed! 🐙
n:ℕhn:3 ∣ n ∨ 3 ∣ n + 1 ∨ 3 ∣ n + 2h0:¬3 ∣ nh1:¬3 ∣ n + 1⊢ 3 ∣ 1 + n ∨ 3 ∣ 2 + n ∨ 3 ∣ 3 + n n:ℕhn:3 ∣ n ∨ 3 ∣ n + 1 ∨ 3 ∣ n + 2h0:¬3 ∣ nh1:¬3 ∣ n + 1h2:3 ∣ n + 2⊢ 3 ∣ 1 + n ∨ 3 ∣ 2 + n ∨ 3 ∣ 3 + nn:ℕhn:3 ∣ n ∨ 3 ∣ n + 1 ∨ 3 ∣ n + 2h0:¬3 ∣ nh1:¬3 ∣ n + 1h2:¬3 ∣ n + 2⊢ 3 ∣ 1 + n ∨ 3 ∣ 2 + n ∨ 3 ∣ 3 + n
n:ℕhn:3 ∣ n ∨ 3 ∣ n + 1 ∨ 3 ∣ n + 2h0:¬3 ∣ nh1:¬3 ∣ n + 1h2:3 ∣ n + 2⊢ 3 ∣ 1 + n ∨ 3 ∣ 2 + n ∨ 3 ∣ 3 + n n:ℕhn:3 ∣ n ∨ 3 ∣ n + 1 ∨ 3 ∣ n + 2h0:¬3 ∣ nh1:¬3 ∣ n + 1h2:3 ∣ n + 2⊢ 3 ∣ 2 + n ∨ 3 ∣ 3 + n
n:ℕhn:3 ∣ n ∨ 3 ∣ n + 1 ∨ 3 ∣ n + 2h0:¬3 ∣ nh1:¬3 ∣ n + 1h2:3 ∣ n + 2⊢ 3 ∣ 2 + n
n:ℕhn:3 ∣ n ∨ 3 ∣ n + 1 ∨ 3 ∣ n + 2h0:¬3 ∣ nh1:¬3 ∣ n + 1h2:3 ∣ 2 + n⊢ 3 ∣ 2 + n
All goals completed! 🐙
n:ℕhn:3 ∣ n ∨ 3 ∣ n + 1 ∨ 3 ∣ n + 2h0:¬3 ∣ nh1:¬3 ∣ n + 1h2:¬3 ∣ n + 2⊢ 3 ∣ 1 + n ∨ 3 ∣ 2 + n ∨ 3 ∣ 3 + n n:ℕhn:3 ∣ n ∨ 3 ∣ n + 1 ∨ 3 ∣ n + 2h0:¬3 ∣ nh1:¬3 ∣ n + 1h2:¬3 ∣ n + 2⊢ False
n:ℕh0:¬3 ∣ nh1:¬3 ∣ n + 1h2:¬3 ∣ n + 2l0:3 ∣ n⊢ Falsen:ℕh0:¬3 ∣ nh1:¬3 ∣ n + 1h2:¬3 ∣ n + 2lr:3 ∣ n + 1 ∨ 3 ∣ n + 2⊢ False
n:ℕh0:¬3 ∣ nh1:¬3 ∣ n + 1h2:¬3 ∣ n + 2l0:3 ∣ n⊢ False All goals completed! 🐙
n:ℕh0:¬3 ∣ nh1:¬3 ∣ n + 1h2:¬3 ∣ n + 2lr:3 ∣ n + 1 ∨ 3 ∣ n + 2⊢ False n:ℕh0:¬3 ∣ nh1:¬3 ∣ n + 1h2:¬3 ∣ n + 2l1:3 ∣ n + 1⊢ Falsen:ℕh0:¬3 ∣ nh1:¬3 ∣ n + 1h2:¬3 ∣ n + 2l2:3 ∣ n + 2⊢ False
n:ℕh0:¬3 ∣ nh1:¬3 ∣ n + 1h2:¬3 ∣ n + 2l1:3 ∣ n + 1⊢ False All goals completed! 🐙
n:ℕh0:¬3 ∣ nh1:¬3 ∣ n + 1h2:¬3 ∣ n + 2l2:3 ∣ n + 2⊢ False All goals completed! 🐙
lemma lem1 (n : ℕ) : (n < 3) → ¬ (Nat.Prime n ∧ Nat.Prime (n + 2) ∧ Nat.Prime (n + 4)) := n:ℕ⊢ n < 3 → ¬(Nat.Prime n ∧ Nat.Prime (n + 2) ∧ Nat.Prime (n + 4))
n:ℕhns3:n < 3⊢ ¬(Nat.Prime n ∧ Nat.Prime (n + 2) ∧ Nat.Prime (n + 4))
n:ℕhns3:n < 3h:Nat.Prime n ∧ Nat.Prime (n + 2) ∧ Nat.Prime (n + 4)⊢ False
n:ℕhns3:n < 3pn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)⊢ False
n:ℕhns3:n < 3pn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)hnge2:2 ≤ n⊢ Falsen:ℕhns3:n < 3pn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)hnge2:¬2 ≤ n⊢ False
n:ℕhns3:n < 3pn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)hnge2:2 ≤ n⊢ False have hne2 : n = 2 := n:ℕ⊢ n < 3 → ¬(Nat.Prime n ∧ Nat.Prime (n + 2) ∧ Nat.Prime (n + 4)) All goals completed! 🐙
n:ℕhns3:n < 3pn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)hnge2:2 ≤ nhne2:n = 2hnp4:¬Nat.Prime 4⊢ False
n:ℕhns3:n < 3pn:Nat.Prime npn2:Nat.Prime (2 + 2)pn4:Nat.Prime (n + 4)hnge2:2 ≤ nhne2:n = 2hnp4:¬Nat.Prime 4⊢ False
n:ℕhns3:n < 3pn:Nat.Prime npn2:Nat.Prime 4pn4:Nat.Prime (n + 4)hnge2:2 ≤ nhne2:n = 2hnp4:¬Nat.Prime 4⊢ False
All goals completed! 🐙
n:ℕhns3:n < 3pn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)hnge2:¬2 ≤ n⊢ False n:ℕhns3:n < 3pn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)hnge2:¬2 ≤ nhnge1:1 ≤ n⊢ Falsen:ℕhns3:n < 3pn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)hnge2:¬2 ≤ nhnge1:¬1 ≤ n⊢ False
n:ℕhns3:n < 3pn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)hnge2:¬2 ≤ nhnge1:1 ≤ n⊢ False have hne1 : n = 1 := n:ℕ⊢ n < 3 → ¬(Nat.Prime n ∧ Nat.Prime (n + 2) ∧ Nat.Prime (n + 4)) All goals completed! 🐙
n:ℕhns3:n < 3pn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)hnge2:¬2 ≤ nhnge1:1 ≤ nhne1:n = 1hnp1:¬Nat.Prime 1⊢ False
n:ℕhns3:n < 3pn:Nat.Prime 1pn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)hnge2:¬2 ≤ nhnge1:1 ≤ nhne1:n = 1hnp1:¬Nat.Prime 1⊢ False
All goals completed! 🐙
n:ℕhns3:n < 3pn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)hnge2:¬2 ≤ nhnge1:¬1 ≤ n⊢ False n:ℕhns3:n < 3pn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)hnge2:¬2 ≤ nhnge1:¬1 ≤ nhnge0:0 ≤ n⊢ Falsen:ℕhns3:n < 3pn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)hnge2:¬2 ≤ nhnge1:¬1 ≤ nhnge0:¬0 ≤ n⊢ False
n:ℕhns3:n < 3pn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)hnge2:¬2 ≤ nhnge1:¬1 ≤ nhnge0:0 ≤ n⊢ False have hne0 : n = 0 := n:ℕ⊢ n < 3 → ¬(Nat.Prime n ∧ Nat.Prime (n + 2) ∧ Nat.Prime (n + 4)) All goals completed! 🐙
n:ℕhns3:n < 3pn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)hnge2:¬2 ≤ nhnge1:¬1 ≤ nhnge0:0 ≤ nhne0:n = 0hnp0:¬Nat.Prime 0⊢ False
n:ℕhns3:n < 3pn:Nat.Prime 0pn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)hnge2:¬2 ≤ nhnge1:¬1 ≤ nhnge0:0 ≤ nhne0:n = 0hnp0:¬Nat.Prime 0⊢ False
All goals completed! 🐙
n:ℕhns3:n < 3pn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)hnge2:¬2 ≤ nhnge1:¬1 ≤ nhnge0:¬0 ≤ n⊢ False All goals completed! 🐙
lemma lem2 (n : ℕ) : (3 < n) → ¬ (Nat.Prime n ∧ Nat.Prime (n + 2) ∧ Nat.Prime (n + 4)) := n:ℕ⊢ 3 < n → ¬(Nat.Prime n ∧ Nat.Prime (n + 2) ∧ Nat.Prime (n + 4))
n:ℕhng3:3 < n⊢ ¬(Nat.Prime n ∧ Nat.Prime (n + 2) ∧ Nat.Prime (n + 4))
n:ℕhng3:3 < nh:Nat.Prime n ∧ Nat.Prime (n + 2) ∧ Nat.Prime (n + 4)⊢ False
n:ℕhng3:3 < npn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)⊢ False
n:ℕhng3:3 < npn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)super:3 ∣ n ∨ 3 ∣ n + 1 ∨ 3 ∣ n + 2⊢ False
n:ℕhng3:3 < npn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)k0:3 ∣ n⊢ Falsen:ℕhng3:3 < npn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)kr:3 ∣ n + 1 ∨ 3 ∣ n + 2⊢ False
n:ℕhng3:3 < npn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)k0:3 ∣ n⊢ False n:ℕhng3:3 < npn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)x:ℕg:n = 3 * x⊢ False
n:ℕhng3:3 < npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)x:ℕg:n = 3 * xu1:¬IsUnit nu2:∀ (a b : ℕ), n = a * b → IsUnit a ∨ IsUnit b⊢ False
n:ℕhng3:3 < npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)x:ℕg:n = 3 * xu1:¬n = 1u2:∀ (a b : ℕ), n = a * b → a = 1 ∨ b = 1⊢ False
n:ℕhng3:3 < npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)x:ℕg:n = 3 * xu1:¬n = 1u2:∀ (a b : ℕ), 3 * x = a * b → a = 1 ∨ b = 1⊢ False
n:ℕhng3:3 < npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)x:ℕg:n = 3 * xu1:¬n = 1u2:∀ (a b : ℕ), 3 * x = a * b → a = 1 ∨ b = 1u3:3 * x = 3 * x → 3 = 1 ∨ x = 1⊢ False
n:ℕhng3:3 < npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)x:ℕg:n = 3 * xu1:¬n = 1u2:∀ (a b : ℕ), 3 * x = a * b → a = 1 ∨ b = 1u3:x = 1⊢ False
n:ℕhng3:3 < npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)x:ℕg:n = 3 * xu1:¬n = 1u2:∀ (a b : ℕ), 3 * x = a * b → a = 1 ∨ b = 1u3:x = 1⊢ False
All goals completed! 🐙
n:ℕhng3:3 < npn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)kr:3 ∣ n + 1 ∨ 3 ∣ n + 2⊢ False n:ℕhng3:3 < npn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)k1:3 ∣ n + 1⊢ Falsen:ℕhng3:3 < npn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)k2:3 ∣ n + 2⊢ False
n:ℕhng3:3 < npn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)k1:3 ∣ n + 1⊢ False n:ℕhng3:3 < npn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)x:ℕg:n + 1 = 3 * x⊢ False
n:ℕhng3:3 < npn:Nat.Prime npn2:Nat.Prime (n + 2)x:ℕg:n + 1 = 3 * xu1:¬IsUnit (n + 4)u2:∀ (a b : ℕ), n + 4 = a * b → IsUnit a ∨ IsUnit b⊢ False
n:ℕhng3:3 < npn:Nat.Prime npn2:Nat.Prime (n + 2)x:ℕg:n + 1 = 3 * xu1:Trueu2:∀ (a b : ℕ), n + 4 = a * b → a = 1 ∨ b = 1⊢ False
n:ℕhng3:3 < npn:Nat.Prime npn2:Nat.Prime (n + 2)x:ℕg:n + 1 = 3 * xu1:Trueu2:∀ (a b : ℕ), n + 4 = a * b → a = 1 ∨ b = 1gp3:n + 4 = 3 * (x + 1)⊢ False
n:ℕhng3:3 < npn:Nat.Prime npn2:Nat.Prime (n + 2)x:ℕg:n + 1 = 3 * xu1:Trueu2:∀ (a b : ℕ), 3 * (x + 1) = a * b → a = 1 ∨ b = 1gp3:n + 4 = 3 * (x + 1)⊢ False
n:ℕhng3:3 < npn:Nat.Prime npn2:Nat.Prime (n + 2)x:ℕg:n + 1 = 3 * xu1:Trueu2:∀ (a b : ℕ), 3 * (x + 1) = a * b → a = 1 ∨ b = 1gp3:n + 4 = 3 * (x + 1)u3:3 * (x + 1) = 3 * (x + 1) → 3 = 1 ∨ x + 1 = 1⊢ False
n:ℕhng3:3 < npn:Nat.Prime npn2:Nat.Prime (n + 2)x:ℕg:n + 1 = 3 * xu1:Trueu2:∀ (a b : ℕ), 3 * (x + 1) = a * b → a = 1 ∨ b = 1gp3:n + 4 = 3 * (x + 1)u3:x = 0⊢ False
n:ℕhng3:3 < npn:Nat.Prime npn2:Nat.Prime (n + 2)x:ℕg:n + 1 = 3 * xu1:Trueu2:∀ (a b : ℕ), 3 * (x + 1) = a * b → a = 1 ∨ b = 1gp3:n + 4 = 3 * (x + 1)u3:x = 0⊢ False
All goals completed! 🐙
n:ℕhng3:3 < npn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)k2:3 ∣ n + 2⊢ False n:ℕhng3:3 < npn:Nat.Prime npn2:Nat.Prime (n + 2)pn4:Nat.Prime (n + 4)x:ℕg:n + 2 = 3 * x⊢ False
n:ℕhng3:3 < npn:Nat.Prime npn4:Nat.Prime (n + 4)x:ℕg:n + 2 = 3 * xu1:¬IsUnit (n + 2)u2:∀ (a b : ℕ), n + 2 = a * b → IsUnit a ∨ IsUnit b⊢ False
n:ℕhng3:3 < npn:Nat.Prime npn4:Nat.Prime (n + 4)x:ℕg:n + 2 = 3 * xu1:Trueu2:∀ (a b : ℕ), n + 2 = a * b → a = 1 ∨ b = 1⊢ False
n:ℕhng3:3 < npn:Nat.Prime npn4:Nat.Prime (n + 4)x:ℕg:n + 2 = 3 * xu1:Trueu2:∀ (a b : ℕ), 3 * x = a * b → a = 1 ∨ b = 1⊢ False
n:ℕhng3:3 < npn:Nat.Prime npn4:Nat.Prime (n + 4)x:ℕg:n + 2 = 3 * xu1:Trueu2:∀ (a b : ℕ), 3 * x = a * b → a = 1 ∨ b = 1u3:3 * x = 3 * x → 3 = 1 ∨ x = 1⊢ False
n:ℕhng3:3 < npn:Nat.Prime npn4:Nat.Prime (n + 4)x:ℕg:n + 2 = 3 * xu1:Trueu2:∀ (a b : ℕ), 3 * x = a * b → a = 1 ∨ b = 1u3:x = 1⊢ False
n:ℕhng3:3 < npn:Nat.Prime npn4:Nat.Prime (n + 4)x:ℕg:n + 2 = 3 * xu1:Trueu2:∀ (a b : ℕ), 3 * x = a * b → a = 1 ∨ b = 1u3:x = 1⊢ False
All goals completed! 🐙
theorem pt_forward (n : ℕ) : Nat.Prime n ∧ Nat.Prime (n + 2) ∧ Nat.Prime (n + 4) → n = 3 := n:ℕ⊢ Nat.Prime n ∧ Nat.Prime (n + 2) ∧ Nat.Prime (n + 4) → n = 3
n:ℕh:Nat.Prime n ∧ Nat.Prime (n + 2) ∧ Nat.Prime (n + 4)⊢ n = 3
n:ℕh:Nat.Prime n ∧ Nat.Prime (n + 2) ∧ Nat.Prime (n + 4)hns3:n < 3⊢ n = 3n:ℕh:Nat.Prime n ∧ Nat.Prime (n + 2) ∧ Nat.Prime (n + 4)hns3:¬n < 3⊢ n = 3
n:ℕh:Nat.Prime n ∧ Nat.Prime (n + 2) ∧ Nat.Prime (n + 4)hns3:n < 3⊢ n = 3 n:ℕh:Nat.Prime n ∧ Nat.Prime (n + 2) ∧ Nat.Prime (n + 4)hns3:n < 3⊢ False
n:ℕh:Nat.Prime n ∧ Nat.Prime (n + 2) ∧ Nat.Prime (n + 4)hns3:n < 3hn:¬(Nat.Prime n ∧ Nat.Prime (n + 2) ∧ Nat.Prime (n + 4))⊢ False
All goals completed! 🐙
n:ℕh:Nat.Prime n ∧ Nat.Prime (n + 2) ∧ Nat.Prime (n + 4)hns3:¬n < 3⊢ n = 3 n:ℕh:Nat.Prime n ∧ Nat.Prime (n + 2) ∧ Nat.Prime (n + 4)hns3:¬n < 3hng3:3 < n⊢ n = 3n:ℕh:Nat.Prime n ∧ Nat.Prime (n + 2) ∧ Nat.Prime (n + 4)hns3:¬n < 3hng3:¬3 < n⊢ n = 3
n:ℕh:Nat.Prime n ∧ Nat.Prime (n + 2) ∧ Nat.Prime (n + 4)hns3:¬n < 3hng3:3 < n⊢ n = 3 n:ℕh:Nat.Prime n ∧ Nat.Prime (n + 2) ∧ Nat.Prime (n + 4)hns3:¬n < 3hng3:3 < n⊢ False
n:ℕh:Nat.Prime n ∧ Nat.Prime (n + 2) ∧ Nat.Prime (n + 4)hns3:¬n < 3hng3:3 < nhn:¬(Nat.Prime n ∧ Nat.Prime (n + 2) ∧ Nat.Prime (n + 4))⊢ False
All goals completed! 🐙
n:ℕh:Nat.Prime n ∧ Nat.Prime (n + 2) ∧ Nat.Prime (n + 4)hns3:¬n < 3hng3:¬3 < n⊢ n = 3 All goals completed! 🐙
theorem pt_backward (n : ℕ) : n = 3 → Nat.Prime n ∧ Nat.Prime (n + 2) ∧ Nat.Prime (n + 4) := n:ℕ⊢ n = 3 → Nat.Prime n ∧ Nat.Prime (n + 2) ∧ Nat.Prime (n + 4)
n:ℕhne3:n = 3⊢ Nat.Prime n ∧ Nat.Prime (n + 2) ∧ Nat.Prime (n + 4)
n:ℕhne3:n = 3⊢ Nat.Prime 3 ∧ Nat.Prime (3 + 2) ∧ Nat.Prime (3 + 4)
n:ℕhne3:n = 3⊢ Nat.Prime 3 ∧ Nat.Prime 5 ∧ Nat.Prime 7
n:ℕhne3:n = 3⊢ Nat.Prime 3n:ℕhne3:n = 3⊢ Nat.Prime 5 ∧ Nat.Prime 7
n:ℕhne3:n = 3⊢ Nat.Prime 3 All goals completed! 🐙
n:ℕhne3:n = 3⊢ Nat.Prime 5 ∧ Nat.Prime 7 n:ℕhne3:n = 3⊢ Nat.Prime 5n:ℕhne3:n = 3⊢ Nat.Prime 7
n:ℕhne3:n = 3⊢ Nat.Prime 5 All goals completed! 🐙
n:ℕhne3:n = 3⊢ Nat.Prime 7 All goals completed! 🐙
theorem prime_tripple (n : ℕ) : Nat.Prime n ∧ Nat.Prime (n + 2) ∧ Nat.Prime (n + 4) ↔ n = 3 := n:ℕ⊢ Nat.Prime n ∧ Nat.Prime (n + 2) ∧ Nat.Prime (n + 4) ↔ n = 3
n:ℕ⊢ Nat.Prime n ∧ Nat.Prime (n + 2) ∧ Nat.Prime (n + 4) → n = 3n:ℕ⊢ n = 3 → Nat.Prime n ∧ Nat.Prime (n + 2) ∧ Nat.Prime (n + 4)
n:ℕ⊢ Nat.Prime n ∧ Nat.Prime (n + 2) ∧ Nat.Prime (n + 4) → n = 3 All goals completed! 🐙
n:ℕ⊢ n = 3 → Nat.Prime n ∧ Nat.Prime (n + 2) ∧ Nat.Prime (n + 4) All goals completed! 🐙
5.6. An equivalence on sets (Emma Reichel, Luisa Caspary)
We have U ⊆ V ↔ U = U ∩ V ↔ V = U ∪ V
. So, the following needs to be proved:
variable (U V : Set α)
example : (U ⊆ V) → U = U ∩ V := α:Type u_1U:Set αV:Set α⊢ U ⊆ V → U = U ∩ V
α:Type u_1U:Set αV:Set αh:U ⊆ V⊢ U = U ∩ V
α:Type u_1U:Set αV:Set αh:U ⊆ Vx:α⊢ x ∈ U ↔ x ∈ U ∩ V
α:Type u_1U:Set αV:Set αh:U ⊆ Vx:α⊢ x ∈ U → x ∈ U ∩ Vα:Type u_1U:Set αV:Set αh:U ⊆ Vx:α⊢ x ∈ U ∩ V → x ∈ U
α:Type u_1U:Set αV:Set αh:U ⊆ Vx:α⊢ x ∈ U → x ∈ U ∩ V α:Type u_1U:Set αV:Set αh:U ⊆ Vx:αhxU:x ∈ U⊢ x ∈ U ∩ V
All goals completed! 🐙
α:Type u_1U:Set αV:Set αh:U ⊆ Vx:α⊢ x ∈ U ∩ V → x ∈ U α:Type u_1U:Set αV:Set αh:U ⊆ Vx:αhxU:x ∈ UhxV:x ∈ V⊢ x ∈ U
All goals completed! 🐙
example : U = U ∩ V → V = U ∪ V:= α:Type u_1U:Set αV:Set α⊢ U = U ∩ V → V = U ∪ V
α:Type u_1U:Set αV:Set αh:U = U ∩ V⊢ V = U ∪ V
α:Type u_1U:Set αV:Set αh:U = U ∩ Vx:α⊢ x ∈ V ↔ x ∈ U ∪ V
α:Type u_1U:Set αV:Set αh:U = U ∩ Vx:α⊢ x ∈ V → x ∈ U ∪ Vα:Type u_1U:Set αV:Set αh:U = U ∩ Vx:α⊢ x ∈ U ∪ V → x ∈ V
α:Type u_1U:Set αV:Set αh:U = U ∩ Vx:α⊢ x ∈ V → x ∈ U ∪ V α:Type u_1U:Set αV:Set αh:U = U ∩ Vx:αhxV:x ∈ V⊢ x ∈ U ∪ V
All goals completed! 🐙
α:Type u_1U:Set αV:Set αh:U = U ∩ Vx:α⊢ x ∈ U ∪ V → x ∈ V α:Type u_1U:Set αV:Set αh:U = U ∩ Vx:αh':x ∈ U ∪ V⊢ x ∈ V
cases h' with
| inl hxU =>
α:Type u_1U:Set αV:Set αh:U = U ∩ Vx:αhxU:x ∈ U ∩ V⊢ x ∈ V
All goals completed! 🐙
| inr hxV => All goals completed! 🐙
example : V = U ∪ V → U ⊆ V := α:Type u_1U:Set αV:Set α⊢ V = U ∪ V → U ⊆ V
α:Type u_1U:Set αV:Set αh:V = U ∪ V⊢ U ⊆ V
α:Type u_1U:Set αV:Set αh:V = U ∪ Vx:αhxU:x ∈ U⊢ x ∈ V
α:Type u_1U:Set αV:Set αh:V = U ∪ Vx:αhxU:x ∈ U⊢ x ∈ U ∪ V
All goals completed! 🐙