diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Parallel.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Parallel.lean index 920aaa1d..e22ffd36 100644 --- a/EuclideanGeometry/Foundation/Axiom/Linear/Parallel.lean +++ b/EuclideanGeometry/Foundation/Axiom/Linear/Parallel.lean @@ -82,16 +82,19 @@ section fig_coecion_parallel /-- Given a nondegenate segment, it is parallel to the ray associated to this nondegenerate segment. -/ theorem SegND.para_toRay (seg_nd : SegND P) : seg_nd ∥ seg_nd.toRay := rfl +/-- Given a nondegenerate segment, it is parallel to its associated directed line. -/ theorem SegND.para_toDirLine (seg_nd : SegND P) : seg_nd ∥ seg_nd.toDirLine := rfl /-- Given a nondegenate segment, it is parallel to the extension line of this nondegenerate segment. -/ theorem SegND.para_toLine (seg_nd : SegND P) : seg_nd ∥ seg_nd.toLine := rfl +/-- Given a ray, the ray is parallel to the directed line associated to the ray. -/ theorem Ray.para_toDirLine (ray : Ray P) : ray ∥ ray.toDirLine := rfl /-- Given a ray, the ray is parallel to the line associated to the ray. -/ theorem Ray.para_toLine (ray : Ray P) : ray ∥ ray.toLine := rfl +/-- A directed line is parallel to the line associated to the directed line. -/ theorem DirLine.para_toLine (dlin : DirLine P) : dlin ∥ dlin.toLine := (DirLine.toLine_toProj_eq_toProj dlin).symm end fig_coecion_parallel @@ -104,85 +107,121 @@ end mk_parallel -- 6 theorems for each coercion, 6 coercion section parallel_iff_coercion_parallel +/-- If two nondegenerate segements are parallel, then their associated rays are parallel. -/ theorem SegND.para_toRay_of_para (seg_nd seg_nd' : SegND P) : seg_nd ∥ seg_nd' → seg_nd.toRay ∥ seg_nd'.toRay := id +/-- If the associated rays of two nondegenerate segments are parallel, then the two segments are parallel. -/ theorem SegND.para_of_para_toRay (seg_nd seg_nd' : SegND P) : seg_nd.toRay ∥ seg_nd'.toRay → seg_nd ∥ seg_nd' := id +/-- Given two nondegenerate segments, they are parallel if and only if their associated rays are parallel. +-/ theorem SegND.para_iff_para_toRay (seg_nd seg_nd' : SegND P) : seg_nd.toRay ∥ seg_nd'.toRay ↔ seg_nd ∥ seg_nd' := ⟨id, id⟩ +/-- If two nondegenerate segments are not parallel, then their associated rays are not parallel. -/ theorem SegND.not_para_toRay_of_not_para (seg_nd seg_nd' : SegND P) : ¬ seg_nd ∥ seg_nd' → ¬ seg_nd.toRay ∥ seg_nd'.toRay := id +/-- If the associated rays of two nondegenerate segments are not parallel, then the two segments are not parallel. -/ theorem SegND.not_para_of_not_para_toRay (seg_nd seg_nd' : SegND P) : ¬ seg_nd.toRay ∥ seg_nd'.toRay → ¬ seg_nd ∥ seg_nd' := id +/-- Given two nondegenerate segments, they are not parallel if and only if their associated rays are not parallel. -/ theorem SegND.not_para_iff_not_para_toRay (seg_nd seg_nd' : SegND P) : ¬ seg_nd ∥ seg_nd' ↔ ¬ seg_nd.toRay ∥ seg_nd'.toRay := ⟨id, id⟩ +/-- If two nondegenerate segments are parallel, then their associated directed lines are parallel. -/ theorem SegND.para_toDirLine_of_para (seg_nd seg_nd' : SegND P) : seg_nd ∥ seg_nd' → seg_nd.toDirLine ∥ seg_nd'.toDirLine := id +/-- If two nondegenerate segments have parallel directed lines, then the segments themselves are parallel. -/ theorem SegND.para_of_para_toDirLine (seg_nd seg_nd' : SegND P) : seg_nd.toDirLine ∥ seg_nd'.toDirLine → seg_nd ∥ seg_nd' := id +/-- Given two nondegenerate segments, their associated direction lines are parallel if and only if the segments are parallel. -/ theorem SegND.para_iff_para_toDirLine (seg_nd seg_nd' : SegND P) : seg_nd.toDirLine ∥ seg_nd'.toDirLine ↔ seg_nd ∥ seg_nd' := ⟨id, id⟩ +/-- If two nondegenerate segments are not parallel, then their associated directed lines are not parallel. -/ theorem SegND.not_para_toDirLine_of_not_para (seg_nd seg_nd' : SegND P) : ¬ seg_nd ∥ seg_nd' → ¬ seg_nd.toDirLine ∥ seg_nd'.toDirLine := id +/-- If the associated directed lines of two nondegenerate segments are not parallel, then the two segments are not parallel. -/ theorem SegND.not_para_of_not_para_toDirLine (seg_nd seg_nd' : SegND P) : ¬ seg_nd.toDirLine ∥ seg_nd'.toDirLine → ¬ seg_nd ∥ seg_nd' := id +/-- Given two nondegenerate segments, they are not parallel if and only if their associated directed lines are not parallel. -/ theorem SegND.not_para_iff_not_para_toDirLine (seg_nd seg_nd' : SegND P) : ¬ seg_nd ∥ seg_nd' ↔ ¬ seg_nd.toDirLine ∥ seg_nd'.toDirLine := ⟨id, id⟩ +/-- If two nondegenerate segments are parallel, then their associated lines are parallel. -/ theorem SegND.para_toLine_of_para (seg_nd seg_nd' : SegND P) : seg_nd ∥ seg_nd' → seg_nd.toLine ∥ seg_nd'.toLine := id +/-- If the lines associated to two nondegenerate segments are parallel, then the two segments are parallel. -/ theorem SegND.para_of_para_toLine (seg_nd seg_nd' : SegND P) : seg_nd.toLine ∥ seg_nd'.toLine → seg_nd ∥ seg_nd' := id +/-- The nondegenerate segments $s$ and $s'$ are parallel if and only if their associated lines are parallel. -/ theorem SegND.para_iff_para_toLine (seg_nd seg_nd' : SegND P) : seg_nd.toLine ∥ seg_nd'.toLine ↔ seg_nd ∥ seg_nd' := ⟨id, id⟩ +/-- Given two nondegenerate segments, if they are not parallel, then their associated lines are not parallel. +-/ theorem SegND.not_para_toLine_of_not_para (seg_nd seg_nd' : SegND P) : ¬ seg_nd ∥ seg_nd' → ¬ seg_nd.toLine ∥ seg_nd'.toLine := id +/-- Given two nondegenerate segments, their asscociated lines are not parallel if and only if they are not parallel. -/ theorem SegND.not_para_of_not_para_toLine (seg_nd seg_nd' : SegND P) : ¬ seg_nd.toLine ∥ seg_nd'.toLine → ¬ seg_nd ∥ seg_nd' := id +/-- This theorem states that two nondegenerate segments are not parallel if and only if their associated lines are not parallel. -/ theorem SegND.not_para_iff_not_para_toLine (seg_nd seg_nd' : SegND P) : ¬ seg_nd ∥ seg_nd' ↔ ¬ seg_nd.toLine ∥ seg_nd'.toLine := ⟨id, id⟩ +/-- If the directed lines associated to two rays are parallel, then the two rays are parallel. -/ theorem Ray.para_of_para_toDirLine (ray ray' : Ray P) : ray.toDirLine ∥ ray'.toDirLine → ray ∥ ray' := id +/-- This theorem states that two rays are parallel if and only if their associated direction lines are parallel. -/ theorem Ray.para_iff_para_toDirLine (ray ray' : Ray P) : ray.toDirLine ∥ ray'.toDirLine ↔ ray ∥ ray' := ⟨id, id⟩ +/-- If two rays are not parallel, then their associated directed lines are not parallel. -/ theorem Ray.not_para_toDirLine_of_not_para (ray ray' : Ray P) : ¬ ray ∥ ray' → ¬ ray.toDirLine ∥ ray'.toDirLine := id +/-- If the directed lines associated to two rays are not parallel, then the two rays are not parallel. -/ theorem Ray.not_para_of_not_para_toDirLine (ray ray' : Ray P) : ¬ ray.toDirLine ∥ ray'.toDirLine → ¬ ray ∥ ray' := id +/-- If two rays are not parallel, then their associated directed lines are not parallel. -/ theorem Ray.not_para_iff_not_para_toDirLine (ray ray' : Ray P) : ¬ ray ∥ ray' ↔ ¬ ray.toDirLine ∥ ray'.toDirLine := ⟨id, id⟩ /-- Given two parallel rays, their extension lines are parallel. -/ theorem Ray.para_toLine_of_para (ray ray' : Ray P) : ray ∥ ray' → ray.toLine ∥ ray'.toLine := id +/-- If the lines associated to two rays are parallel, then thew two rays are parallel. -/ theorem Ray.para_of_para_toLine (ray ray' : Ray P) : ray.toLine ∥ ray'.toLine → ray ∥ ray' := id +/-- The extension lines of two rays are parallel if and only if the rays themselves are parallel. -/ theorem Ray.para_iff_para_toLine (ray ray' : Ray P) : ray.toLine ∥ ray'.toLine ↔ ray ∥ ray' := ⟨id, id⟩ /-- Given two rays, if their extension lines are not parallel, they are not parallel. -/ theorem Ray.not_para_toLine_of_not_para (ray ray' : Ray P) : ¬ ray ∥ ray' → ¬ ray.toLine ∥ ray'.toLine := id +/-- If two rays have non-parallel associated lines, then the rays themselves are not parallel. -/ theorem Ray.not_para_of_not_para_toLine (ray ray' : Ray P) : ¬ ray.toLine ∥ ray'.toLine → ¬ ray ∥ ray' := id +/-- This theorem states that two rays are not parallel if and only if their associated lines are not parallel. -/ theorem Ray.not_para_iff_not_para_toLine (ray ray' : Ray P) : ¬ ray ∥ ray' ↔ ¬ ray.toLine ∥ ray'.toLine := ⟨id, id⟩ +/-- If two directed lines are parallel, then their associated lines are also parallel. -/ theorem DirLine.para_toLine_of_para {l₁ l₂ : DirLine P} (h : l₁ ∥ l₂) : l₁.toLine ∥ l₂.toLine := by induction l₁ using DirLine.ind induction l₂ using DirLine.ind exact h +/-- Given two directed lines $l_1$ and $l_2$, if their associated lines are parallel, then the two directed lines are parallel. -/ theorem DirLine.para_of_para_toLine {l₁ l₂ : DirLine P} (h : l₁.toLine ∥ l₂.toLine) : l₁ ∥ l₂ := by induction l₁ using DirLine.ind induction l₂ using DirLine.ind exact h +/-- Given two directed lines $l_1$ and $l_2$, $l_1$ is parallel to $l_2$ if and only if the underlying lines of $l_1$ and $l_2$ are parallel. +-/ theorem DirLine.para_toLine_iff_para (l₁ l₂ : DirLine P) : l₁.toLine ∥ l₂.toLine ↔ l₁ ∥ l₂ := ⟨para_of_para_toLine, para_toLine_of_para⟩ +/-- The non-parallelism of two direction lines $l_1$ and $l_2$ is equivalent to the non-parallelism of their associated lines. -/ theorem DirLine.not_para_toLine_iff_not_para (l₁ l₂ : DirLine P) : ¬ l₁.toLine ∥ l₂.toLine ↔ ¬ l₁ ∥ l₂ := (para_toLine_iff_para l₁ l₂).not +/-- Given two directed lines l₁ and l₂, if they are not parallel, then their associated lines are not parallel. -/ theorem DirLine.not_para_toLine_of_not_para {l₁ l₂ : DirLine P} (h : ¬ l₁ ∥ l₂) : ¬ l₁.toLine ∥ l₂.toLine := (not_para_toLine_iff_not_para l₁ l₂).mpr h +/-- Given two directed lines l₁ and l₂, if their associated lines are not parallel, then the two directed lines are not parallel. -/ theorem DirLine.not_para_of_not_para_toLine {l₁ l₂ : DirLine P} (h : ¬ l₁.toLine ∥ l₂.toLine) : ¬ l₁ ∥ l₂ := (not_para_toLine_iff_not_para l₁ l₂).mp h @@ -190,92 +229,122 @@ end parallel_iff_coercion_parallel section reverse -variable {α β : Type*} [DirFig α P] [DirFig β P] {l₁ : α} {l₂ : β} +variable {α β : Type*} [DirFig α P] [DirFig β P] +-- Add `iff` theorems and @[simp] -theorem DirFig.para_rev_of_para (h : l₁ ∥ l₂) : l₁ ∥ reverse l₂ := +/-- For two parallel directed figures $l_1$ and $l_2$, $l_1$ is parallel to the reverse of $l_2$. -/ +theorem DirFig.para_rev_of_para {l₁ : α} {l₂ : β} (h : l₁ ∥ l₂) : l₁ ∥ reverse l₂ := h.trans (rev_toProj_eq_toProj l₂).symm +/-- Given two nondegenerate segments, if they are parallel, then the reverse of the second segment is parallel to the first segment. -/ theorem SegND.para_rev_of_para {s s' : SegND P} (h : s ∥ s') : s ∥ s'.reverse := DirFig.para_rev_of_para h +/-- If two rays are parallel, then one ray is parallel to the reverse of the other ray. -/ theorem Ray.para_rev_of_para {r r' : Ray P} (h : r ∥ r') : r ∥ r'.reverse := DirFig.para_rev_of_para h -theorem DirLine.para_rev_of_para {l l' : DirLine P} (h : l ∥ l') : l ∥ l'.reverse := +/-- Given two parallel directed lines $l_1$ and $l_2$, $l_1$ is parallel to the reverse of $l_2$. -/ +theorem DirLine.para_rev_of_para {l₁ l₂ : DirLine P} (h : l₁ ∥ l₂) : l₁ ∥ l₂.reverse := DirFig.para_rev_of_para h -theorem DirFig.not_para_rev_of_not_para (h : ¬ l₁ ∥ l₂) : ¬ l₁ ∥ reverse l₂ := +/-- For two directed figures $l_1$ and $l_2$, if they are not parallel, then $l_1$ is not parallel to the reverse of $l_2$. -/ +theorem DirFig.not_para_rev_of_not_para {l₁ : α} {l₂ : β} (h : ¬ l₁ ∥ l₂) : ¬ l₁ ∥ reverse l₂ := fun hn ↦ h ((para_rev_of_para hn).trans (congrArg ProjObj.toProj (rev_rev))) +/-- If two nondegenerate segments $s$ and $s'$ are not parallel, then $s$ is not parallel to the reverse of $s'$. -/ theorem SegND.not_para_rev_of_not_para {s s' : SegND P} (h : ¬ s ∥ s') : ¬ s ∥ s'.reverse := DirFig.not_para_rev_of_not_para h +/-- Given two rays, if their extension lines are not parallel, they are not parallel. -/ theorem Ray.not_para_rev_of_not_para {r r' : Ray P} (h : ¬ r ∥ r') : ¬ r ∥ r'.reverse := DirFig.not_para_rev_of_not_para h +/-- If two directed lines $l$ and $l'$ are not parallel, then $l$ is not parallel to the reverse of $l'$. -/ theorem DirLine.not_para_rev_of_not_para {l l' : DirLine P} (h : ¬ l ∥ l') : ¬ l ∥ l'.reverse := DirFig.not_para_rev_of_not_para h -theorem DirFig.rev_para_of_para (h : l₁ ∥ l₂) : reverse l₁ ∥ l₂ := +/-- If $l_1$ and $l_2$ are two parallel directed figure, then the reverse of $l_1$ is parallel to $l_2$. -/ +theorem DirFig.rev_para_of_para {l₁ : α} {l₂ : β} (h : l₁ ∥ l₂) : reverse l₁ ∥ l₂ := (rev_toProj_eq_toProj l₁).trans h +/-- Given two nondegenerate segments $s$ and $s'$, if they are parallel, then the reverse of $s$ is parallel to $s'$. -/ theorem SegND.rev_para_of_para {s s' : SegND P} (h : s ∥ s') : s.reverse ∥ s' := DirFig.rev_para_of_para h +/-- If two rays $r$ and $r'$ are parallel, then the reverse of $r$ is parallel to $r'$. -/ theorem Ray.rev_para_of_para {r r' : Ray P} (h : r ∥ r') : r.reverse ∥ r' := DirFig.rev_para_of_para h +/-- If two directed lines $l$ and $l'$ are parallel, then the reverse of $l$ is parallel to $l'$. -/ theorem DirLine.rev_para_of_para {l l' : DirLine P} (h : l ∥ l') : l.reverse ∥ l' := DirFig.rev_para_of_para h -theorem DirFig.not_rev_para_of_not_para (h : ¬ l₁ ∥ l₂) : ¬ reverse l₁ ∥ l₂ := +/-- Given two directed figures $l_1$ and $l_2$, if they are not parallel, then the reverse of $l_1$ is not parallel to $l_2$. -/ +theorem DirFig.not_rev_para_of_not_para {l₁ : α} {l₂ : β} (h : ¬ l₁ ∥ l₂) : ¬ reverse l₁ ∥ l₂ := fun hn ↦ h ((congrArg ProjObj.toProj rev_rev).symm.trans (rev_para_of_para hn) ) +/-- Given two nondegenerate segments, if they are not parallel, then reverse of the first segment is not parallel to the second segment. -/ theorem SegND.not_rev_para_of_not_para {s s' : SegND P} (h : ¬ s ∥ s') : ¬ s.reverse ∥ s' := DirFig.not_rev_para_of_not_para h +/-- Given two rays $r$ and $r'$, if they are not parallel, then the reverse of $r$ is not parallel to $r'$. -/ theorem Ray.not_rev_para_of_not_para {r r' : Ray P} (h : ¬ r ∥ r') : ¬ r.reverse ∥ r' := DirFig.not_rev_para_of_not_para h +/-- Given two directed lines $l$ and $l'$, if they are not parallel, then the reverse of $l$ is not parallel to $l'$. -/ theorem DirLine.not_rev_para_of_not_para {l l' : DirLine P} (h : ¬ l ∥ l') : ¬ l.reverse ∥ l' := DirFig.not_rev_para_of_not_para h -theorem DirFig.rev_para_rev_of_para (h : l₁ ∥ l₂) : reverse l₁ ∥ reverse l₂ := +/-- If two directed figures $l_1$ and $l_2$ are parallel, then the reverse of $l_1$ is parallel to the reverse of $l_2$. -/ +theorem DirFig.rev_para_rev_of_para {l₁ : α} {l₂ : β} (h : l₁ ∥ l₂) : reverse l₁ ∥ reverse l₂ := rev_para_of_para (para_rev_of_para h) +/--`AI` Given two nondegenerate segments $s$ and $s'$, if they are parallel, then their reverses are parallel. -/ theorem SegND.rev_para_rev_of_para {s s' : SegND P} (h : s ∥ s') : s.reverse ∥ s'.reverse := DirFig.rev_para_rev_of_para h +/-- If two rays are parallel, then their reverse rays are also parallel. -/ theorem Ray.rev_para_rev_of_para {r r' : Ray P} (h : r ∥ r') : r.reverse ∥ r'.reverse := DirFig.rev_para_rev_of_para h +/-- If two directed lines $l_1$ and $l_2$ are parallel, then their reverses are parallel. -/ theorem DirLine.rev_para_rev_of_para {l l' : DirLine P} (h : l ∥ l') : l.reverse ∥ l'.reverse := DirFig.rev_para_rev_of_para h -theorem DirFig.not_rev_para_rev_of_not_para (h : ¬ l₁ ∥ l₂) : ¬ reverse l₁ ∥ reverse l₂ := +/-- Given two unparallel directed figures, then their reverses are not parallel either. -/ +theorem DirFig.not_rev_para_rev_of_not_para {l₁ : α} {l₂ : β} (h : ¬ l₁ ∥ l₂) : ¬ reverse l₁ ∥ reverse l₂ := not_rev_para_of_not_para (not_para_rev_of_not_para h) +/-- Given two nondegenerate segments, if they are not parallel, then their reverses are not parallel. -/ theorem SegND.not_rev_para_rev_of_not_para {s s' : SegND P} (h : ¬ s ∥ s') : ¬ s.reverse ∥ s'.reverse := DirFig.not_rev_para_rev_of_not_para h +/-- Given two rays $r$ and $r'$, if they are not parallel, then their reverse rays are not parallel. -/ theorem Ray.not_rev_para_rev_of_not_para {r r' : Ray P} (h : ¬ r ∥ r') : ¬ r.reverse ∥ r'.reverse := DirFig.not_rev_para_rev_of_not_para h +/-- Given two unparallel lines, their reverses are not parallel. -/ theorem DirLine.not_rev_para_rev_of_not_para {l l' : DirLine P} (h : ¬ l ∥ l') : ¬ l.reverse ∥ l'.reverse := DirFig.not_rev_para_rev_of_not_para h -theorem DirFig.para_rev_iff_para : l₁ ∥ reverse l₂ ↔ l₁ ∥ l₂ := sorry +/-- Given two directed figures $l_1$ and $l_2$, $l_1$ is parallel to the reverse of $l_2$ if and only if $l_1$ is parallel to $l_2$. -/ +theorem DirFig.para_rev_iff_para {l₁ : α} {l₂ : β} : l₁ ∥ reverse l₂ ↔ l₁ ∥ l₂ := sorry +/-- Given two nondegenerate segments $s$ and $s'$, $s$ is parallel to the reverse of $s'$ if and only if $s$ is parallel to $s'$. -/ @[simp] theorem SegND.para_rev_iff_para {s s' : SegND P} : s ∥ s'.reverse ↔ s ∥ s' := sorry +/-- Given two rays $r$ and $r'$, $r$ is parallel to the reverse of $r'$ if and only if $r$ is parallel to $r'$. -/ @[simp] theorem Ray.para_rev_iff_para {r r' : Ray P} : r ∥ r'.reverse ↔ r ∥ r' := sorry +/-- Given two directed lines $l$ and $l'$, $l$ is parallel to the reverse of $l'$ if and only if $l$ and $l'$ are parallel. -/ @[simp] theorem DirLine.para_rev_iff_para {l l' : DirLine P} : l ∥ l'.reverse ↔ l ∥ l' := sorry -theorem DirFig.not_para_rev_iff_not_para : ¬ l₁ ∥ reverse l₂ ↔ ¬ l₁ ∥ l₂ := +/-- For two directed figures $l_1$ and $l_2$, $l_1$ is not parallel to the reverse of $l_2$ if and only if $l_1$ is not parallel to $l_2$. -/ +theorem DirFig.not_para_rev_iff_not_para {l₁ : α} {l₂ : β} : ¬ l₁ ∥ reverse l₂ ↔ ¬ l₁ ∥ l₂ := para_rev_iff_para.not @[simp] @@ -290,7 +359,7 @@ theorem Ray.not_para_rev_iff_not_para {r r' : Ray P} : ¬ r ∥ r'.reverse ↔ theorem DirLine.not_para_rev_iff_not_para {l l' : DirLine P} : ¬ l ∥ l'.reverse ↔ ¬ l ∥ l' := para_rev_iff_para.not -theorem DirFig.rev_para_iff_para : reverse l₁ ∥ l₂ ↔ l₁ ∥ l₂ := sorry +theorem DirFig.rev_para_iff_para {l₁ : α} {l₂ : β} : reverse l₁ ∥ l₂ ↔ l₁ ∥ l₂ := sorry @[simp] theorem SegND.rev_para_iff_para {s s' : SegND P} : s.reverse ∥ s' ↔ s ∥ s':= sorry @@ -301,7 +370,7 @@ theorem Ray.rev_para_iff_para {r r' : Ray P} : r.reverse ∥ r' ↔ r ∥ r' := @[simp] theorem DirLine.rev_para_iff_para {l l' : DirLine P} : l.reverse ∥ l' ↔ l ∥ l' := sorry -theorem DirFig.not_rev_para_iff_not_para : ¬ reverse l₁ ∥ l₂ ↔ ¬ l₁ ∥ l₂ := +theorem DirFig.not_rev_para_iff_not_para {l₁ : α} {l₂ : β} : ¬ reverse l₁ ∥ l₂ ↔ ¬ l₁ ∥ l₂ := rev_para_iff_para.not @[simp] @@ -316,7 +385,7 @@ theorem Ray.not_rev_para_iff_not_para {r r' : Ray P} : ¬ r.reverse ∥ r' ↔ theorem DirLine.not_rev_para_iff_not_para {l l' : DirLine P} : ¬ l.reverse ∥ l' ↔ ¬ l ∥ l' := rev_para_iff_para.not -theorem DirFig.rev_para_rev_iff_para : reverse l₁ ∥ reverse l₂ ↔ l₁ ∥ l₂ := sorry +theorem DirFig.rev_para_rev_iff_para {l₁ : α} {l₂ : β} : reverse l₁ ∥ reverse l₂ ↔ l₁ ∥ l₂ := sorry @[simp] theorem SegND.rev_para_rev_iff_para {s s' : SegND P} : s.reverse ∥ s'.reverse ↔ s ∥ s' := sorry @@ -328,7 +397,7 @@ theorem Ray.rev_para_rev_iff_para {r r' : Ray P} : r.reverse ∥ r'.reverse ↔ theorem DirLine.rev_para_rev_iff_para {l l' : DirLine P} : l.reverse ∥ l'.reverse ↔ l ∥ l' := sorry -theorem DirFig.not_rev_para_rev_iff_not_para : ¬ reverse l₁ ∥ reverse l₂ ↔ ¬ l₁ ∥ l₂ := +theorem DirFig.not_rev_para_rev_iff_not_para {l₁ : α} {l₂ : β} : ¬ reverse l₁ ∥ reverse l₂ ↔ ¬ l₁ ∥ l₂ := rev_para_rev_iff_para.not @[simp] @@ -351,34 +420,41 @@ section intersection_of_line section construction +/-- Given three vectors $\vec u$, $\vec v$ and $\vec w$, we may write $\vec w$ as a linear combination of $\vec u$ and $\vec v$ (usually), i.e. $\vec w = c_u \vec u + c_v \vec v$. This function returns $c_u$, which we call the \emph{first linear coefficients} later on. When $\vec u$ and $\vec v$ are linearly dependent, we return $0$. -/ def cu (u v w: Vec) : ℝ := (Vec.det u v)⁻¹ * (Vec.det w v) +/-- Given three vectors $\vec u$, $\vec v$ and $\vec w$, we may write $\vec w$ as a linear combination of $\vec u$ and $\vec v$ (usually), i.e. $\vec w = c_u \vec u + c_v \vec v$. This function returns $c_v$, which we call the \emph{second linear coefficients} later on. When $\vec u$ and $\vec v$ are linearly dependent, we return $0$. -/ def cv (u v w: Vec) : ℝ := (Vec.det u v)⁻¹ * (Vec.det u w) +/-- Given three vectors $\vec u$, $\vec v$ and $\vec w$, the first linear coefficients to write $\vec w$ in terms of $\vec u$ and $\vec v$ is the same as the second linear coefficients to write $\vec w$ in terms of $\vec v$ and $\vec u$, i.e. after reversing the two base vectors. -/ theorem cu_cv (u v w : Vec) : cu u v w = cv v u w := by rw [cu, cv, ← Vec.det_skew v u, inv_neg, Vec.det_apply w v, Vec.det_apply v w] field_simp ring +/-- Given three vectors $\vec u$, $\vec v$, and $\vec w$, if we change $\vec w$ to $-\vec w$, then the first linear combination coefficients is negated. -/ theorem cu_neg (u v w : Vec) : cu u v (- w) = - cu u v w := by rw [cu, cu, neg_mul_eq_mul_neg, map_neg] rfl -theorem Vec.linear_combination_of_not_collinear' {u v w : Vec} (hu : v ≠ 0) (h' : ¬(∃ (t : ℝ), u = t • v)) : w = cu u v w • u + cv u v w • v := by +/-- Let $\vec u$, $\vec v$ and $\vec w$ be three vectors such that $\vec v$ is nonzero and $\vec u$ is not a multiple of $\vec v$, then $\vec w$ is the linear combination of $\vec u$ and $\vec v$ with the first and second linear coefficients respectively, i.e. $\vec w = c_u(\vec u, \vec v, \vec w) \cdot \vec u + c_v(\vec u, \vec v, \vec w) \cdot \vec v$. -/ +theorem Vec.linear_combination_of_not_colinear' {u v w : Vec} (hu : v ≠ 0) (h' : ¬(∃ (t : ℝ), u = t • v)) : w = cu u v w • u + cv u v w • v := by have : u.fst * v.snd - u.snd * v.fst ≠ 0 := (det_eq_zero_iff_eq_smul_right.not.mpr (not_or.mpr ⟨hu, h'⟩)) dsimp [cu, cv, det_apply] apply Vec.ext <;> · field_simp ring -theorem Vec.linear_combination_of_not_collinear_vecND {u v : VecND} (w : Vec) (h' : VecND.toProj u ≠ VecND.toProj v) : w = (cu u.1 v.1 w) • u.1 + (cv u.1 v.1 w) • v.1 := by +/-- Given two nondegenerate vectors $\vec u$ and $\vec v$ of distinct projective directions, any vector $w$ is the linear combination of $\vec u$ and $\vec v$ with coefficients, namely, $\vec w = c_u(\vec u, \vec v, \vec w) \vec u + c_v(\vec u, \vec v, \vec w) \vec v$. -/ +theorem Vec.linear_combination_of_not_colinear_vecND {u v : VecND} (w : Vec) (h' : VecND.toProj u ≠ VecND.toProj v) : w = (cu u.1 v.1 w) • u.1 + (cv u.1 v.1 w) • v.1 := by have h₁ : ¬(∃ (t : ℝ), u.1 = t • v.1) · by_contra h₂ let _ := VecND.toProj_eq_toProj_iff.2 h₂ tauto - exact @linear_combination_of_not_collinear' u.1 v.1 w v.2 h₁ + exact @linear_combination_of_not_colinear' u.1 v.1 w v.2 h₁ -theorem Vec.linear_combination_of_not_collinear_dir {u v : Dir} (w : Vec) (h' : u.toProj ≠ v.toProj) : w = (cu u.unitVec v.unitVec w) • u.unitVec + (cv u.unitVec v.unitVec w) • v.unitVec := by +/-- Given two directions $\vec u$ and $\vec v$ of different projective directions, any vector $w$ is the linear combination of $\vec u$ and $\vec v$ with coefficients, namely, $\vec w = c_u(\vec u, \vec v, \vec w) \vec u + c_v(\vec u, \vec v, \vec w) \vec v$. -/ +theorem Vec.linear_combination_of_not_colinear_dir {u v : Dir} (w : Vec) (h' : u.toProj ≠ v.toProj) : w = (cu u.unitVec v.unitVec w) • u.unitVec + (cv u.unitVec v.unitVec w) • v.unitVec := by have h₁ : (u.toProj ≠ v.toProj) → ¬(∃ (t : ℝ), u.unitVec = t • v.unitVec) · by_contra h push_neg at h @@ -396,18 +472,19 @@ theorem Vec.linear_combination_of_not_collinear_dir {u v : Dir} (w : Vec) (h' : have hv3 : v.unitVec = v'.1 := rfl rw [hu3, hv3, ←hu2, ←hv2, ← VecND.toProj_eq_toProj_iff] at h tauto - exact @linear_combination_of_not_collinear' u.unitVec v.unitVec w (VecND.ne_zero _) (h₁ h') + exact @linear_combination_of_not_colinear' u.unitVec v.unitVec w (VecND.ne_zero _) (h₁ h') -/-- Given two unparallel rays, this function gives the intersection of their extension lines. -/ -def inx_of_extn_line (r₁ r₂ : Ray P) (_h : ¬ r₁ ∥ r₂) : P := (cu r₁.toDir.unitVecND r₂.toDir.unitVecND (VEC r₁.source r₂.source) • r₁.toDir.unitVec +ᵥ r₁.source) +-- This function in fact does not require $r_1$ and $r_2$ to be unparallel, but please only use this under the unparallel assumption.` +/-- Given two unparallel rays, this function returns the intersection of their associated lines. -/ +def inx_of_extn_line (r₁ r₂ : Ray P) (_h: ¬ r₁ ∥ r₂) : P := (cu r₁.toDir.unitVecND r₂.toDir.unitVecND (VEC r₁.source r₂.source) • r₁.toDir.unitVec +ᵥ r₁.source) -/-- Given two unparallel rays, we define the intersection of their extension lines. -/ +/-- Given two unparallel rays $r_1$ and $r_2$, the intersection of the lines of $r_1$ and $r_2$ is the same as the intersection of the lines of $r_2$ and $r_1$. -/ theorem inx_of_extn_line_symm (r₁ r₂ : Ray P) (h : ¬ r₁ ∥ r₂) : inx_of_extn_line r₁ r₂ h = inx_of_extn_line r₂ r₁ (Ne.symm h) := by have hsymm : cu r₁.toDir.unitVecND r₂.toDir.unitVecND (VEC r₁.source r₂.source) • r₁.toDir.unitVec = cu r₂.toDir.unitVecND r₁.toDir.unitVecND (VEC r₂.source r₁.source) • r₂.toDir.unitVec + (r₂.source -ᵥ r₁.source) - · have h := Vec.linear_combination_of_not_collinear_dir (VEC r₁.source r₂.source) (Ne.symm h) + · have h := Vec.linear_combination_of_not_colinear_dir (VEC r₁.source r₂.source) (Ne.symm h) nth_rw 1 [← cu_cv, Vec.mkPtPt] at h rw [h, ← neg_vec r₁.source r₂.source, cu_neg, neg_smul] exact eq_neg_add_of_add_eq rfl @@ -432,11 +509,12 @@ theorem inx_lies_on_snd_extn_line (r₁ r₂ : Ray P) (h : ¬ r₁ ∥ r₂) : ( rw [inx_of_extn_line_symm] exact inx_lies_on_fst_extn_line r₂ r₁ (Ne.symm h) -/-- Given two rays $r_1$ $r_2$, if they have same projective directions and the source of $r_1$ lies on the extension line of $r_2$, then the two rays have same extension lines. -/ +/-- Given two rays $r_1$ and $r_2$, if they have the same projective direction and the source of $r_1$ lies on the extension line of $r_2$, then the two rays have same extension lines. -/ theorem ray_toLine_eq_of_same_extn_line {r₁ r₂ : Ray P} (h : same_extn_line r₁ r₂) : r₁.toLine = r₂.toLine := (Quotient.eq (r := same_extn_line.setoid)).mpr h + -- `key theorem` -/-- Given four rays $a_1$ $a_2$ $b_1$ $b_2$, if $a_1$ $a_2$ have the same extension line, $b_1$ $b_2$ have the same extension line , $a_1$ $b_1$ have different projective directions and $a_2$ $b_2$ have different projective directions, then the intersection of extension lines of $a_1$ $b_1$ is same as that of $a_2$ $b_2$ -/ +/-- Let $a_1$, $a_2$, $b_1$, and $b_2$ be four rays such that $a_1$ and $a_2$ have the same extension line and $b_1$ and $b_2$ have the same extension line. If $a_1$ is not parallel to $b_1$ and $a_2$ is not parallel to $b_2$, then the intersection of extension lines of $a_1$ and $b_1$ is same as that of $a_2$ and $b_2$ -/ theorem inx_eq_of_same_extn_line {a₁ b₁ a₂ b₂ : Ray P} (g₁ : same_extn_line a₁ a₂) (g₂ : same_extn_line b₁ b₂) (h₁ : ¬ a₁ ∥ b₁ ) (h₂ : ¬ a₂ ∥ b₂) : inx_of_extn_line a₁ b₁ h₁ = inx_of_extn_line a₂ b₂ h₂ := by have ha1 : inx_of_extn_line a₁ b₁ h₁ LiesOn a₁.toLine := inx_lies_on_fst_extn_line a₁ b₁ h₁ have hb1 : inx_of_extn_line a₁ b₁ h₁ LiesOn b₁.toLine := inx_lies_on_snd_extn_line a₁ b₁ h₁ @@ -455,7 +533,7 @@ theorem heq_of_inx_of_extn_line (a₁ b₁ a₂ b₂ : Ray P) (h₁ : same_extn_ rw [h₁.1, h₂.1] exact @heq_funext (Ray.toProj a₁ ≠ Ray.toProj b₁) (Ray.toProj a₂ ≠ Ray.toProj b₂) P e (fun h => inx_of_extn_line a₁ b₁ h) (fun h => inx_of_extn_line a₂ b₂ h) (inx_eq_of_same_extn_line h₁ h₂) -/-- Given two lines with different projective directions, this function gives the intersection point of these two lines. -/ +/-- Given two unparallel lines, this function returns the intersection point of these two lines. -/ def Line.inx (l₁ l₂ : Line P) (h : ¬ l₁ ∥ l₂) : P := @Quotient.hrecOn₂ (Ray P) (Ray P) same_extn_line.setoid same_extn_line.setoid (fun l l' => (Line.toProj l ≠ Line.toProj l') → P) l₁ l₂ inx_of_extn_line heq_of_inx_of_extn_line h /-- Given two unparallel line $l_1$ $l_2$, the point given by function "Line.inx" lies on $l_1$ -/ @@ -466,7 +544,7 @@ theorem Line.inx_lies_on_fst {l₁ l₂ : Line P} (h : ¬ l₁ ∥ l₂) : simp only [← hr1, ← hr2] exact inx_lies_on_fst_extn_line r1 r2 (by rw [← hr1, ← hr2] at h; exact h) -/-- Given two unparallel line $l_1$ $l_2$, the point given by function "Line.inx" lies on $l_1$ -/ +/-- Given two unparallel line $l_1$ $l_2$, the point given by function "Line.inx" lies on $l_2$ -/ theorem Line.inx_lies_on_snd {l₁ l₂ : Line P} (h : ¬ l₁ ∥ l₂) : Line.inx l₁ l₂ h LiesOn l₂ := by rcases Quotient.exists_rep l₁ with ⟨r1, hr1⟩ @@ -484,7 +562,7 @@ section property -- In this section, we discuss the property of intersection point using `is_inx` instead of `Line.inx`. As a corollory, we deduce the symmetry of Line.inx. -/-- Two unparallel lines have only one intersection point -/ +/-- Two unparallel lines have only one intersection point, i.e. if two points $A$ and $B$ are both intersection points of unparallel lines $l_1$ and $l_2$, then $B = A$. -/ theorem unique_of_inx_of_line_of_not_para {A B : P} {l₁ l₂ : Line P} (h : ¬ l₁ ∥ l₂) (a : is_inx A l₁ l₂) (b : is_inx B l₁ l₂) : B = A := Classical.byContradiction fun d ↦ h (congrArg Line.toProj (eq_of_pt_pt_lies_on_of_ne (_h := ⟨d⟩) a.1 b.1 a.2 b.2)) @@ -492,15 +570,15 @@ theorem unique_of_inx_of_line_of_not_para {A B : P} {l₁ l₂ : Line P} (h : ¬ theorem inx_of_line_eq_inx {A : P} {l₁ l₂ : Line P} (h : ¬ l₁ ∥ l₂) (ha : is_inx A l₁ l₂) : A = l₁.inx l₂ h := unique_of_inx_of_line_of_not_para h (Line.inx_is_inx h) ha -/-- The symmetry of Line.inx -/ +/-- The symmetry of Line.inx, i.e. for two unparallel lines $l_1$ and $l_2$, the intersection of $l_1$ with $l_2$ is the same as the intersection of $l_2$ with $l_1$. -/ theorem Line.inx.symm {l₁ l₂ : Line P} (h : ¬ l₁ ∥ l₂) : Line.inx l₂ l₁ (Ne.symm h) = Line.inx l₁ l₂ h := unique_of_inx_of_line_of_not_para h (Line.inx_is_inx h) (is_inx.symm (Line.inx_is_inx (Ne.symm h))) -/-- If two parallel lines share a same point, they are exactly the same line -/ +/-- If two parallel lines share a same point, they are exactly the same line. -/ theorem eq_of_parallel_and_pt_lies_on {A : P} {l₁ l₂ : Line P} (h₁ : A LiesOn l₁) (h₂ : A LiesOn l₂) (h : l₁ ∥ l₂) : l₁ = l₂ := eq_of_same_toProj_and_pt_lies_on h₁ h₂ h -/-- If two lines are not parallel, then their intersection is not empty -/ +/-- If two lines are not parallel, then their intersection is not empty, i.e. there exists a point that lies on both lines. -/ theorem exists_intersection_of_nonparallel_lines {l₁ l₂ : Line P} (h : ¬ l₁ ∥ l₂) : ∃ p : P, p LiesOn l₁ ∧ p LiesOn l₂ := by rcases l₁.nontriv with ⟨A, ⟨B, hab⟩⟩ rcases l₂.nontriv with ⟨C, ⟨D, hcd⟩⟩ @@ -512,7 +590,7 @@ theorem exists_intersection_of_nonparallel_lines {l₁ l₂ : Line P} (h : ¬ l let x := cu (VEC A B) (VEC C D) (VEC A C) let y := cv (VEC A B) (VEC C D) (VEC A C) have e : VEC A C = x • VEC A B + y • VEC C D := by - apply Vec.linear_combination_of_not_collinear_vecND (VEC A C) e' + apply Vec.linear_combination_of_not_colinear_vecND (VEC A C) e' have h : VEC C (x • VEC A B +ᵥ A) = - y • VEC C D := by rw [← vec_sub_vec A _ _, vec_of_pt_vadd_pt_eq_vec _ _, e] simp only [Complex.real_smul, sub_add_cancel', neg_smul] @@ -520,7 +598,7 @@ theorem exists_intersection_of_nonparallel_lines {l₁ l₂ : Line P} (h : ¬ l (collinear_of_vec_eq_smul_vec (vec_of_pt_vadd_pt_eq_vec A _)), (lies_on_iff_collinear_of_ne_lies_on_lies_on hcd.1 hcd.2.1 _).2 (collinear_of_vec_eq_smul_vec h)⟩ -/-- If two lines are not parallel, then there exists a unique point in their intersection -/ +/-- If two lines are not parallel, then there exists a unique point in their intersection. -/ theorem exists_unique_intersection_of_nonparallel_lines {l₁ l₂ : Line P} (h : ¬ l₁ ∥ l₂) : ∃! p : P, p LiesOn l₁ ∧ p LiesOn l₂ := by rcases exists_intersection_of_nonparallel_lines h with ⟨X, ⟨h₁, h₂⟩⟩ use X diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Perpendicular.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Perpendicular.lean index e667681b..c83fe34e 100644 --- a/EuclideanGeometry/Foundation/Axiom/Linear/Perpendicular.lean +++ b/EuclideanGeometry/Foundation/Axiom/Linear/Perpendicular.lean @@ -8,9 +8,11 @@ open Line variable {P : Type _} [EuclideanPlane P] {α β γ : Type*} [ProjObj α] [ProjObj β] [ProjObj γ] {l₁ : α} {l₂ : β} {l₃ : γ} +/-- This defines two projective objects to be perpendicular, i.e. their associated projective directions are perpendicular. -/ def perpendicular (l₁ : α) (l₂ : β) : Prop := ProjObj.toProj l₁ = (ProjObj.toProj l₂).perp +/-- Abbreviate `perpendicular $l_1$ $l_2$` to `$l_1$ IsPerpendicularTo $l_2$` or `$l_1$ $\perp$ $l_2$`. -/ scoped infix : 50 " IsPerpendicularTo " => perpendicular scoped infix : 50 " ⟂ " => perpendicular @@ -28,6 +30,7 @@ end Notation namespace perpendicular +/-- A projective object $l$ is not perpendicular to itself. -/ @[simp] protected theorem irrefl (l : α) : ¬ (l ⟂ l) := sorry @@ -41,6 +44,7 @@ end perpendicular section Perpendicular_and_parallel +/-- If $l_1$ is perpendicular to $l_2$ and $l_2$ is perpendicular to $l_3$, then $l_1$ is perpendicular to $l_3$. -/ theorem parallel_of_perp_perp (h₁ : l₁ ⟂ l₂) (h₂ : l₂ ⟂ l₃) : l₁ ∥ l₃ := by unfold perpendicular at h₂ simp only [perpendicular, h₂, Proj.perp_perp] at h₁ @@ -50,6 +54,7 @@ theorem perp_of_parallel_perp (h₁ : l₁ ∥ l₂) (h₂ : l₂ ⟂ l₃) : l theorem perp_of_perp_parallel (h₁ : l₁ ⟂ l₂) (h₂ : l₂ ∥ l₃) : l₁ ⟂ l₃ := h₁.trans (congrArg Proj.perp h₂) +/-- If $l_1$ is perpendicular to $l_2$, then they have different projective direction. -/ theorem toProj_ne_toProj_of_perp (h : l₁ ⟂ l₂) : ProjObj.toProj l₁ ≠ ProjObj.toProj l₂ := sorry @@ -59,23 +64,26 @@ end Perpendicular_and_parallel section Perpendicular_constructions +/-- Given a point $A$ and a line $l$, this function returns the line through $A$ perpendicular to $l$. -/ def perp_line (A : P) (l : Line P) := Line.mk_pt_proj A (l.toProj.perp) @[simp] theorem toProj_of_perp_line_eq_toProj_perp (A : P) (l : Line P) : (perp_line A l).toProj = l.toProj.perp := proj_eq_of_mk_pt_proj A l.toProj.perp +/-- For a point $A$ and a line $l$, the line through $A$ perpendicular to $l$ constructed using `perp_line` is perpendicular to $l$. -/ theorem perp_line_perp (A : P) (l : Line P) : perp_line A l ⟂ l := toProj_of_perp_line_eq_toProj_perp A l +/-- For a point $A$ and a line $l$, the projective direction of $l$ is different from the projective direction of the line through $A$ perpendicular to $l$. -/ theorem toProj_ne_perp_toProj (A : P) (l : Line P) : l.toProj ≠ (perp_line A l).toProj := Ne.trans_eq (perpendicular.irrefl l) (toProj_of_perp_line_eq_toProj_perp A l).symm +/-- For a point $A$ and a line $l$, this function returns the perpendicular foot from $A$ to $l$. -/ def perp_foot (A : P) (l : Line P) : P := Line.inx l (perp_line A l) (toProj_ne_perp_toProj A l) -def dist_pt_line (A : P) (l : Line P) := Seg.length (SEG A (perp_foot A l)) - theorem perp_foot_lies_on_line (A : P) (l : Line P) : perp_foot A l LiesOn l := (Line.inx_is_inx _).1 +/-- Given a point $A$ and a line $l$, the perpendicular foot from $A$ to $l$ is the same as $A$ if and only if $A$ lies on $l$. -/ theorem perp_foot_eq_self_iff_lies_on (A : P) (l : Line P) : perp_foot A l = A ↔ A LiesOn l := ⟨ fun h ↦ Eq.mpr (h.symm ▸ Eq.refl (A LiesOn l)) (perp_foot_lies_on_line A l), fun h ↦ (inx_of_line_eq_inx _ ⟨h, (pt_lies_on_of_mk_pt_proj A (Proj.perp (Line.toProj l)))⟩).symm⟩ @@ -87,18 +95,24 @@ theorem pt_ne_iff_not_lies_on_of_eq_perp_foot {A B : P} {l : Line P} (h : B = pe rw [h] exact (perp_foot_ne_self_iff_not_lies_on A l) +/-- If a point $A$ does not lie on a line $l$, then the line through $A$ and the perpendicular root from $A$ to $l$ is the line through $A$ perpendicular to $l$. -/ theorem line_of_self_perp_foot_eq_perp_line_of_not_lies_on {A : P} {l : Line P} (h : ¬ A LiesOn l) : LIN A (perp_foot A l) ((perp_foot_ne_self_iff_not_lies_on A l).2 h) = perp_line A l := eq_line_of_pt_pt_of_ne (_h := ⟨(perp_foot_ne_self_iff_not_lies_on A l).2 h⟩) (pt_lies_on_of_mk_pt_proj A l.toProj.perp) (Line.inx_is_inx (toProj_ne_perp_toProj A l)).2 -theorem line_of_self_perp_foot_perp_line_of_not_lies_on {A : P} {l : Line P} (h : ¬ A LiesOn l) : LIN A (perp_foot A l) ((perp_foot_ne_self_iff_not_lies_on A l).2 h) ⟂ l := +/-- If a point $A$ does on lie on a line $l$, the line through $A$ and the perpendicular roort from $A$ to $l$ is perpendicular to $l$. -/ +theorem line_of_self_perp_foot_perp_line_of_not_lies_on {A : P} {l : Line P} (h : ¬ (A LiesOn l)) : LIN A (perp_foot A l) ((perp_foot_ne_self_iff_not_lies_on A l).2 h) ⟂ l := (congrArg toProj (line_of_self_perp_foot_eq_perp_line_of_not_lies_on h)).trans (perp_line_perp A l) +/-- This function returns the distance from a point $A$ to a line $l$, as the distance between $A$ and the perpendicular root from $A$ to $l$. -/ +def dist_pt_line (A : P) (l : Line P) := Seg.length (SEG A (perp_foot A l)) + theorem dist_eq_zero_iff_lies_on (A : P) (l : Line P) : dist_pt_line A l = 0 ↔ A LiesOn l := Seg.length_eq_zero_iff_deg.trans (perp_foot_eq_self_iff_lies_on A l) theorem perp_foot_unique {A B : P} {l : DirLine P} (h : B LiesOn l) [_hne : PtNe A B] (hp : LIN A B ⟂ l) : perp_foot A l = B := sorry --- `Maybe the proof of following theorems should require the Pythagorean Theorem.` +-- Maybe the proof of this theorem should require the Pythagorean Theorem. +/-- Let $B$ be a point on a line $l$, then the distance from a point $A$ to $B$ is greater or equal to the distance from $A$ to $l$. -/ theorem dist_pt_line_shortest (A B : P) {l : Line P} (h : B LiesOn l) : dist A B ≥ dist_pt_line A l := sorry theorem eq_dist_eq_perp_foot {A B : P} {l : DirLine P} (h : A LiesOn l) (heq : dist B A = dist_pt_line B l) : A = perp_foot B l := sorry @@ -133,7 +147,7 @@ theorem inner_product_eq_zero_of_perp (v w : VecND) (h : v ⟂ w) : inner v.1 w. unfold perpendicular Proj.perp at h rw [Proj.vadd_coe_left] at h erw [Proj.map_vecND_toProj] at h - simp only [Dir.map_apply, ne_eq, LinearEquiv.restrictScalars_apply, VecND.toDir_toProj] at h + simp only [Dir.map_apply, ne_eq, LinearEquiv.restrictScalars_apply, VecND.toDir_toProj] at h erw [VecND.toProj_eq_toProj_iff] at h obtain ⟨ ⟨ xv, yv ⟩, hv ⟩ := v obtain ⟨ ⟨ xw, yw ⟩, hw ⟩ := w