Part 1 of 2

TheoremA discrete subgroup is a lattice iff it has full rank#✓fully proved

Let \(E\) be a finite-dimensional real normed space and let \(L \subseteq E\) be a \(\mathbb{Z}\)-submodule (an additive subgroup) that is discrete in the subspace topology. Then the \(\mathbb{Z}\)-rank of \(L\) equals \(\dim_{\mathbb{R}} E\) if and only if \(L\) is a \(\mathbb{Z}\)-lattice in \(E\), that is, \(L\) spans \(E\) over \(\mathbb{R}\).

theorem discrete_full_rank_iff_isZLattice {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E)
    [DiscreteTopology L] :
    Module.finrank ℤ L = Module.finrank ℝ E ↔ IsZLattice ℝ L

Sources

ATLAS NumberTheoryI, Lemma 14.3 (full-rank clause only).

TheoremErdős–Anning theorem#✓fully proved

An infinite set of points in the plane with pairwise integer distances is collinear.

theorem erdos_anning :
    ∀ (S : Set (EuclideanSpace ℝ (Fin 2))), S.Infinite →
      (∀ p ∈ S, ∀ q ∈ S, ∃ n : ℕ, dist p q = (n : ℝ)) → Collinear ℝ S

Sources

N. H. Anning and P. Erdős, "Integral distances," Bull. Amer. Math. Soc. 51 (1945), 598–600; P. Erdős, "Integral distances," Bull. Amer. Math. Soc. 51 (1945), 996. Overview: https://en.wikipedia.org/wiki/Erd%C5%91s%E2%80%93Anning_theorem

TheoremEuler's polyhedron formula#●ready to prove

Let \(V\), \(E\) and \(F\) be finite sets, let \(\iota : V \to \mathbb{R}^3\) be an injective map into Euclidean space, and let \(P = \operatorname{conv} \iota(V)\) be the convex hull of its image; assume \(P\) has nonempty interior \(\operatorname{int} P\), and write \(\partial P\) for its frontier. Each edge \(e \in E\) has an ordered pair of endpoints \((s(e), t(e)) \in V \times V\), with segment \([e] = [\iota(s(e)), \iota(t(e))]\); each face \(f \in F\) has a finite vertex set \(V_f \subseteq V\), with cell \(C_f = \operatorname{conv} \iota(V_f)\). Say that the segment between vertices \(u, w \in V\) lies in the face \(f\) when \(u, w \in V_f\) and \([\iota(u), \iota(w)] \subseteq C_f\), and that it lies in exactly two faces when it lies in two distinct faces \(f_1, f_2\) and every face it lies in is \(f_1\) or \(f_2\). Assume the following. For every edge \(e\): \([e] \subseteq P\); \(s(e) \ne t(e)\); if \(\iota(v) \in [e]\) for a vertex \(v\), then \(v = s(e)\) or \(v = t(e)\); and the segment between \(s(e)\) and \(t(e)\) lies in exactly two faces. Distinct edges \(e_1, e_2\) never have the same endpoints, in the same or in the reverse order, and every common point of \([e_1]\) and \([e_2]\) is \(\iota(v)\) for a vertex \(v\) that is an endpoint of both. Every vertex is an endpoint of some edge. For every face \(f\): \(C_f \subseteq P\); \(V_f\) has at least \(3\) elements; \(C_f \cap \operatorname{int} P = \emptyset\); the affine span of \(C_f\) has dimension \(2\); and every \(v \in V_f\) is an endpoint of two distinct edges whose segments are contained in \(C_f\). For distinct faces \(f_1, f_2\), \(V_{f_1} \not\subseteq V_{f_2}\), and every point of \(C_{f_1} \cap C_{f_2}\) is \(\iota(v)\) for some vertex \(v\) or lies on \([e]\) for some edge \(e\). The cells cover the frontier: \(\partial P \subseteq \bigcup_{f \in F} C_f\). Finally, if \(v_1 \ne v_2\) are vertices such that \([\iota(v_1), \iota(v_2)] \subseteq P\), this segment is disjoint from \(\operatorname{int} P\), it contains \(\iota(v)\) only for \(v \in \{v_1, v_2\}\), and it lies in exactly two faces, then some edge has endpoints \((v_1, v_2)\) or \((v_2, v_1)\). Then \(|V| - |E| + |F| = 2\).

The vertex set may contain points that are not extreme points of \(P\), such as subdivision vertices on an edge or inside a face of the polyhedron, and the faces may subdivide a face of \(P\) (for example by a diagonal); the statement concerns this cellulation, and \(E\) and \(F\) need not be the edges and facets of \(P\).

MetaMathlibExt.euler_polyhedron_formula · 74 lines

theorem_wanted euler_polyhedron_formula
    {V E F : Type*} [Fintype V] [Fintype E] [Fintype F]
    (P : Set (EuclideanSpace Real (Fin 3)))
    (emb : V → EuclideanSpace Real (Fin 3))
    (hemb : Function.Injective emb)
    (hP : P = convexHull Real (Set.range emb))
    (hinterior : (interior P).Nonempty)
    (edgeEndpoints : E → V × V)
    (hEdge : ∀ e, segment Real (emb (edgeEndpoints e).1) (emb (edgeEndpoints e).2) ⊆ P)
    (hEdge_ne : ∀ e, (edgeEndpoints e).1 ≠ (edgeEndpoints e).2)
    (hEdge_atomic : ∀ (e : E) (v : V),
      emb v ∈ segment Real (emb (edgeEndpoints e).1) (emb (edgeEndpoints e).2) →
      v = (edgeEndpoints e).1 ∨ v = (edgeEndpoints e).2)
    (hEdge_inter : ∀ e₁ e₂, e₁ ≠ e₂ → ∀ x,
      x ∈ segment Real (emb (edgeEndpoints e₁).1) (emb (edgeEndpoints e₁).2) →
      x ∈ segment Real (emb (edgeEndpoints e₂).1) (emb (edgeEndpoints e₂).2) →
      ∃ v : V, emb v = x ∧
        (v = (edgeEndpoints e₁).1 ∨ v = (edgeEndpoints e₁).2) ∧
        (v = (edgeEndpoints e₂).1 ∨ v = (edgeEndpoints e₂).2))
    (faceVertices : F → Finset V)
    (hFace : ∀ f, convexHull Real (emb '' ↑(faceVertices f)) ⊆ P)
    (hFace_card : ∀ f, 3 ≤ (faceVertices f).card)
    (hVert_edge : ∀ v, ∃ e, (edgeEndpoints e).1 = v ∨ (edgeEndpoints e).2 = v)
    (hFace_bdry : ∀ f, convexHull Real (emb '' ↑(faceVertices f)) ∩ interior P = ∅)
    (hFace_dim : ∀ f, Module.finrank Real
      (affineSpan Real (convexHull Real (emb '' ↑(faceVertices f)))).direction = 2)
    (hFace_cover : frontier P ⊆
      Set.iUnion (fun f => convexHull Real (emb '' ↑(faceVertices f))))
    (hEdge_two_faces : ∀ e, ∃ f₁ f₂, f₁ ≠ f₂ ∧
      (edgeEndpoints e).1 ∈ faceVertices f₁ ∧
      (edgeEndpoints e).2 ∈ faceVertices f₁ ∧
      segment Real (emb (edgeEndpoints e).1) (emb (edgeEndpoints e).2) ⊆
        convexHull Real (emb '' ↑(faceVertices f₁)) ∧
      (edgeEndpoints e).1 ∈ faceVertices f₂ ∧
      (edgeEndpoints e).2 ∈ faceVertices f₂ ∧
      segment Real (emb (edgeEndpoints e).1) (emb (edgeEndpoints e).2) ⊆
        convexHull Real (emb '' ↑(faceVertices f₂)) ∧
      ∀ f, ((edgeEndpoints e).1 ∈ faceVertices f ∧
        (edgeEndpoints e).2 ∈ faceVertices f ∧
        segment Real (emb (edgeEndpoints e).1) (emb (edgeEndpoints e).2) ⊆
          convexHull Real (emb '' ↑(faceVertices f))) → f = f₁ ∨ f = f₂)
    (hEdge_no_rev : ∀ e₁ e₂, (edgeEndpoints e₁ = edgeEndpoints e₂ ∨
      ((edgeEndpoints e₁).1 = (edgeEndpoints e₂).2 ∧
       (edgeEndpoints e₁).2 = (edgeEndpoints e₂).1)) → e₁ = e₂)
    (hEdge_complete : ∀ v₁ v₂ : V, v₁ ≠ v₂ →
      segment Real (emb v₁) (emb v₂) ⊆ P →
      segment Real (emb v₁) (emb v₂) ∩ interior P = ∅ →
      (∀ v : V, emb v ∈ segment Real (emb v₁) (emb v₂) → v = v₁ ∨ v = v₂) →
      (∃ f₁ f₂ : F,
        f₁ ≠ f₂ ∧ v₁ ∈ faceVertices f₁ ∧ v₂ ∈ faceVertices f₁ ∧
        segment Real (emb v₁) (emb v₂) ⊆
          convexHull Real (emb '' ↑(faceVertices f₁)) ∧
        v₁ ∈ faceVertices f₂ ∧ v₂ ∈ faceVertices f₂ ∧
        segment Real (emb v₁) (emb v₂) ⊆
          convexHull Real (emb '' ↑(faceVertices f₂)) ∧
        ∀ f : F, (v₁ ∈ faceVertices f ∧ v₂ ∈ faceVertices f ∧
          segment Real (emb v₁) (emb v₂) ⊆
            convexHull Real (emb '' ↑(faceVertices f))) → f = f₁ ∨ f = f₂) →
      ∃ e : E, edgeEndpoints e = (v₁, v₂) ∨ edgeEndpoints e = (v₂, v₁))
    (hFace_incomparable :
      ∀ f₁ f₂, f₁ ≠ f₂ → ¬ (faceVertices f₁ ⊆ faceVertices f₂))
    (hFace_inter : ∀ f₁ f₂, f₁ ≠ f₂ → ∀ x,
      x ∈ convexHull Real (emb '' ↑(faceVertices f₁)) →
      x ∈ convexHull Real (emb '' ↑(faceVertices f₂)) →
      (∃ v, emb v = x) ∨
        (∃ e, x ∈ segment Real (emb (edgeEndpoints e).1) (emb (edgeEndpoints e).2)))
    (hFace_boundary : ∀ f, ∀ v ∈ faceVertices f, ∃ e₁ e₂, e₁ ≠ e₂ ∧
      ((edgeEndpoints e₁).1 = v ∨ (edgeEndpoints e₁).2 = v) ∧
      ((edgeEndpoints e₂).1 = v ∨ (edgeEndpoints e₂).2 = v) ∧
      segment Real (emb (edgeEndpoints e₁).1) (emb (edgeEndpoints e₁).2) ⊆
        convexHull Real (emb '' ↑(faceVertices f)) ∧
      segment Real (emb (edgeEndpoints e₂).1) (emb (edgeEndpoints e₂).2) ⊆
        convexHull Real (emb '' ↑(faceVertices f)))
    : (Fintype.card V : Int) - (Fintype.card E : Int) + (Fintype.card F : Int) = 2

Sources

https://en.wikipedia.org/wiki/Euler_characteristic.

TheoremMonsky's theorem#✓fully proved

Let \(T\) be a finite set of subsets of the Euclidean plane \(\mathbb{R}^2\) such that every member of \(T\) is the convex hull of three points \(a, b, c\) of the plane (not necessarily distinct), the union of the members of \(T\) is the closed unit square \([0,1]^2\), any two distinct members of \(T\) have disjoint interiors, and all members of \(T\) have the same Lebesgue measure. Then the number of members of \(T\) is even.

Proof: A 2-adic valuation on ℝ gives a three-colouring of the plane, and a Sperner-type parity count supplies a rainbow triangle whose area valuation rules out an odd number of pieces.

theorem monsky_theorem :
    ∀ (T : Finset (Set (EuclideanSpace ℝ (Fin 2)))),
      (∀ t ∈ T, ∃ a b c : EuclideanSpace ℝ (Fin 2), t = convexHull ℝ {a, b, c}) →
      Set.sUnion (↑T : Set (Set (EuclideanSpace ℝ (Fin 2)))) =
        {x | ∀ i, 0 ≤ x.ofLp i ∧ x.ofLp i ≤ 1} →
      (↑T : Set (Set (EuclideanSpace ℝ (Fin 2)))).PairwiseDisjoint interior →
      (∃ A : ENNReal, ∀ t ∈ T, MeasureTheory.volume t = A) →
      Even T.card

Sources

Paul Monsky, "On Dividing A Square Into Triangles," The American Mathematical Monthly 77(2) (1970), 161–164, DOI 10.1080/00029890.1970.11992441.

Uses 2

Proof usesDeterminant formula for the area of a triangle · Area of the unit square

3 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.