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.

declaration uses 'sorry'example (n : ℕ) :
    ∑ k ≤ n, k * k = n * (n + 1) * (2*n + 1) / 6 := byn:ℕ⊢ ∑ k ∈ Finset.Iic n, k * k = n * (n + 1) * (2 * n + 1) / 6
  sorryAll goals completed! 🐙

declaration uses 'sorry'example (n : ℕ) :
    ∑ k ≤ n, k * k * k = n * n * (n + 1) * (n + 1) / 4 := byn:ℕ⊢ ∑ k ∈ Finset.Iic n, k * k * k = n * n * (n + 1) * (n + 1) / 4
  sorryAll goals completed! 🐙

declaration uses 'sorry'example (n : ℕ) : ∑ k ≤ n, 2 * k - 1 = sorry := byn:ℕ⊢ ∑ k ∈ Finset.Iic n, 2 * k - 1 = sorry
  sorryAll goals completed! 🐙

declaration uses 'sorry'example (n : ℕ) : ∏ k ≤ n, (1 + 1 / (k + 1)) = sorry := byn:ℕ⊢ ∏ k ∈ Finset.Iic n, (1 + 1 / (k + 1)) = sorry
  sorryAll goals completed! 🐙

declaration uses 'sorry'example (q : ℝ) (hq : abs q  < 1) :
    Filter.Tendsto (fun n ↦ q^n) atTop (nhds 0) := byatTop:Filter ℕq:ℝhq:|q| < 1⊢ Filter.Tendsto (fun n => q ^ n) atTop (nhds 0)
  sorryAll goals completed! 🐙

5.2. Own addition on ℚ (Adrian Eckstein und Debora Ortlieb)

def own_add (a b : ℚ) : ℚ := a * b + 2 * a + 2 * b + 2

notation a " ⊕ " b:60 => own_add a b

lemma declaration uses 'sorry'own_mul_komm (a b : ℚ) : (a ⊕ b) = b ⊕ a := bya:ℚb:ℚ⊢ a ⊕ b = b ⊕ a
  sorryAll goals completed! 🐙

lemma declaration uses 'sorry'own_mul_assoc (a b c : ℚ) :
    ((a ⊕ b) ⊕ c) = a ⊕ (b ⊕ c) := bya:ℚb:ℚc:ℚ⊢ (a ⊕ b) ⊕ c = a ⊕ b ⊕ c

  sorryAll goals completed! 🐙

lemma declaration uses 'sorry'own_mul_right_neutral (a : ℚ) : (a ⊕ (-1)) = a := bya:ℚ⊢ a ⊕ -1 = a
  sorryAll goals completed! 🐙

lemma declaration uses 'sorry'own_mul_left_neutral (a : ℚ) : ((-1) ⊕ a) = a := bya:ℚ⊢ (-1) ⊕ a = a
  sorryAll goals completed! 🐙

declaration uses 'sorry'example (n : ℕ) : ∏ k ≤ n, (1 - 1 / (k + 1)) = sorry := byn:ℕ⊢ ∏ k ∈ Finset.Iic n, (1 - 1 / (k + 1)) = sorry
  sorryAll goals completed! 🐙

5.3. Fixed points and contractions (Jule Kiesele, Anna Vitiello)

variable {α : Type*} [MetricSpace α]  (f : α → α)
    (h_con : ∃ q < 1, ∀ x y, dist (f x) (f y) ≤
      q * dist x y) (x y : α)

declaration uses 'sorry'example (hxy : f x = f y) : x = y := byα:Type u_1inst✝:MetricSpace αf:α → αh_con:∃ q < 1, ∀ (x y : α), dist (f x) (f y) ≤ q * dist x yx:αy:αhxy:f x = f y⊢ x = y
  sorryAll goals completed! 🐙

variable [CompleteSpace α]

declaration uses 'sorry'example : ∃ x, f x = x := byα:Type u_1inst✝¹:MetricSpace αf:α → αh_con:∃ q < 1, ∀ (x y : α), dist (f x) (f y) ≤ q * dist x yx:αy:αinst✝:CompleteSpace α⊢ ∃ x, f x = x
  sorryAll goals completed! 🐙

5.4. 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 := byX:Type u_2inst✝:TopologicalSpace XA:Set X⊢ IsPathConnected A ↔ IsPathConnected' A
  constructormpX:Type u_2inst✝:TopologicalSpace XA:Set X⊢ IsPathConnected A → IsPathConnected' AmprX:Type u_2inst✝:TopologicalSpace XA:Set X⊢ IsPathConnected' A → IsPathConnected A
  ·mpX:Type u_2inst✝:TopologicalSpace XA:Set X⊢ IsPathConnected A → IsPathConnected' A -- Mathlib ⇒ Intuitive
    intro ⟨p1, ⟨hp1, h1⟩⟩mpX:Type u_2inst✝:TopologicalSpace XA:Set Xp1:Xhp1:p1 ∈ Ah1:∀ {y : X}, y ∈ A → JoinedIn A p1 y⊢ IsPathConnected' A
    -- show that the set is nonempty
    refine ⟨⟨p1, hp1⟩, ?_⟩mpX:Type u_2inst✝: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 : ↑(Icc 0 1)), γ t ∈ A
    intro p2 p3 hp2 hp3mpX:Type u_2inst✝: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 : ↑(Icc 0 1)), γ t ∈ A
    -- construct a path from p2 to p3 by using the
    -- transitivity of the JoinedIn relation
    obtain ⟨γ, hγ⟩ := (h1 hp2).symm.trans (h1 hp3)mp.introX:Type u_2inst✝: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 : ↑(Icc 0 1)), γ t ∈ A
    exact ⟨γ, γ.continuous, γ.source, γ.target, hγ⟩All goals completed! 🐙
  ·mprX:Type u_2inst✝:TopologicalSpace XA:Set X⊢ IsPathConnected' A → IsPathConnected A -- Intuitive ⇒ Mathlib
    rintro ⟨hne, hC⟩mpr.introX:Type u_2inst✝:TopologicalSpace XA:Set Xhne:A.NonemptyhC:∀ (x y : X), x ∈ A → y ∈ A → ∃ γ, Continuous γ ∧ γ 0 = x ∧ γ 1 = y ∧ ∀ (t : ↑(Icc 0 1)), γ t ∈ A⊢ IsPathConnected A
    obtain ⟨x, hx⟩ := hnempr.intro.introX:Type u_2inst✝:TopologicalSpace XA:Set XhC:∀ (x y : X), x ∈ A → y ∈ A → ∃ γ, Continuous γ ∧ γ 0 = x ∧ γ 1 = y ∧ ∀ (t : ↑(Icc 0 1)), γ t ∈ Ax:Xhx:x ∈ A⊢ IsPathConnected A
    refine ⟨x, hx, fun {y} hy => ?_⟩mpr.intro.introX:Type u_2inst✝:TopologicalSpace XA:Set XhC:∀ (x y : X), x ∈ A → y ∈ A → ∃ γ, Continuous γ ∧ γ 0 = x ∧ γ 1 = y ∧ ∀ (t : ↑(Icc 0 1)), γ t ∈ Ax:Xhx:x ∈ Ay:Xhy:y ∈ A⊢ JoinedIn A x y
    obtain ⟨γ, γ_cont, γ0, γ1, hγ⟩ := hC x y hx hympr.intro.intro.intro.intro.intro.introX:Type u_2inst✝:TopologicalSpace XA:Set XhC:∀ (x y : X), x ∈ A → y ∈ A → ∃ γ, Continuous γ ∧ γ 0 = x ∧ γ 1 = y ∧ ∀ (t : ↑(Icc 0 1)), γ t ∈ Ax:Xhx:x ∈ Ay:Xhy:y ∈ Aγ:↑(Icc 0 1) → Xγ_cont:Continuous γγ0:γ 0 = xγ1:γ 1 = yhγ:∀ (t : ↑(Icc 0 1)), γ t ∈ A⊢ JoinedIn A x y
    -- construct a Path type from my intuitive definition
    let p : Path x y := {
      toFun := γ,
      continuous_toFun := γ_cont,
      source' := γ0,
      target' := γ1
    }mpr.intro.intro.intro.intro.intro.introX:Type u_2inst✝:TopologicalSpace XA:Set XhC:∀ (x y : X), x ∈ A → y ∈ A → ∃ γ, Continuous γ ∧ γ 0 = x ∧ γ 1 = y ∧ ∀ (t : ↑(Icc 0 1)), γ t ∈ Ax:Xhx:x ∈ Ay:Xhy:y ∈ Aγ:↑(Icc 0 1) → Xγ_cont:Continuous γγ0:γ 0 = xγ1:γ 1 = yhγ:∀ (t : ↑(Icc 0 1)), γ t ∈ Ap:_root_.Path x y := { toFun := γ, continuous_toFun := γ_cont, source' := γ0, target' := γ1 }⊢ JoinedIn A x y
    exact ⟨p, hγ⟩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) := byX:Type u_2inst✝:TopologicalSpace XA:Set XB:Set XhA:IsPathConnected AhB:IsPathConnected BhAB:(A ∩ B).Nonempty⊢ IsPathConnected (A ∪ B)
  -- select a point z in the intersection
  obtain ⟨x, hxA, hxB⟩ := hABintro.introX:Type u_2inst✝:TopologicalSpace XA:Set XB:Set XhA:IsPathConnected AhB:IsPathConnected Bx:XhxA:x ∈ AhxB:x ∈ B⊢ IsPathConnected (A ∪ B)
  use xhX:Type u_2inst✝: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
  refine ⟨Set.mem_union_left B hxA , fun {y} hy => ?_⟩hX:Type u_2inst✝: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
  rcases hy with hyA | hyBh.inlX:Type u_2inst✝:TopologicalSpace XA:Set XB:Set XhA:IsPathConnected AhB:IsPathConnected Bx:XhxA:x ∈ AhxB:x ∈ By:XhyA:y ∈ A⊢ JoinedIn (A ∪ B) x yh.inrX:Type u_2inst✝:TopologicalSpace XA:Set XB:Set XhA:IsPathConnected AhB:IsPathConnected Bx:XhxA:x ∈ AhxB:x ∈ By:XhyB:y ∈ B⊢ JoinedIn (A ∪ B) x y
  ·h.inlX:Type u_2inst✝: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
    have joinedInA := hA.joinedIn x hxA y hyAh.inlX:Type u_2inst✝: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
    exact joinedInA.mono subset_union_leftAll goals completed! 🐙
  ·h.inrX:Type u_2inst✝: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
    have joinedInB := hB.joinedIn x hxB y hyBh.inrX:Type u_2inst✝: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
    exact joinedInB.mono subset_union_rightAll goals completed! 🐙

end PathConnected

5.5. Parallel inequality (Moritz Graßnitzer, Natalie Jahnes)

Parallel inequality, or a homomorphism is injective iff its kernel is trivial.

5.6. 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.

declaration uses 'sorry'example (n : ℕ) :
    Nat.Prime n ∧ Nat.Prime (n + 2) ∧
    Nat.Prime (n + 4) → n = 3 := byα:Type u_1inst✝¹:MetricSpace αf:α → αh_con:∃ q < 1, ∀ (x y : α), dist (f x) (f y) ≤ q * dist x yx:αy:αinst✝:CompleteSpace αn:ℕ⊢ Nat.Prime n ∧ Nat.Prime (n + 2) ∧ Nat.Prime (n + 4) → n = 3
  sorryAll goals completed! 🐙

5.7. 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 α)

declaration uses 'sorry'example : (U ⊆ V) → U = U ∩ V := byα:Type u_1inst✝¹:MetricSpace αf:α → αh_con:∃ q < 1, ∀ (x y : α), dist (f x) (f y) ≤ q * dist x yx:αy:αinst✝:CompleteSpace αU:Set αV:Set α⊢ U ⊆ V → U = U ∩ V
  sorryAll goals completed! 🐙

declaration uses 'sorry'example : U = U ∩ V → V = U ∪ V:= byα:Type u_1inst✝¹:MetricSpace αf:α → αh_con:∃ q < 1, ∀ (x y : α), dist (f x) (f y) ≤ q * dist x yx:αy:αinst✝:CompleteSpace αU:Set αV:Set α⊢ U = U ∩ V → V = U ∪ V
  sorryAll goals completed! 🐙

declaration uses 'sorry'example : V = U ∪ V → U ⊆ V := byα:Type u_1inst✝¹:MetricSpace αf:α → αh_con:∃ q < 1, ∀ (x y : α), dist (f x) (f y) ≤ q * dist x yx:αy:αinst✝:CompleteSpace αU:Set αV:Set α⊢ V = U ∪ V → U ⊆ V
  sorryAll goals completed! 🐙