def EuclidGeom.Perpendicular {α : Type u_2} {β : Type u_3} [EuclidGeom.ProjObj α] [EuclidGeom.ProjObj β] (l₁ : α) (l₂ : β) : Prop

This defines two projective objects to be perpendicular, i.e. their associated projective directions are perpendicular.

Equations

• EuclidGeom.Perpendicular l₁ l₂ = (EuclidGeom.toProj l₁ = (EuclidGeom.toProj l₂).perp)

def EuclidGeom.term_IsPerpendicularTo_ : Lean.TrailingParserDescr

Abbreviate Perpendicular $l_1$ $l_2$ to $l_1$ IsPerpendicularTo $l_2$ or $l_1$ $\perp$ $l_2$.

Equations

• One or more equations did not get rendered due to their size.

def EuclidGeom.«term_⟂_» : Lean.TrailingParserDescr

Equations

• EuclidGeom.«term_⟂_» = Lean.ParserDescr.trailingNode `EuclidGeom.term_⟂_ 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⟂ ") (Lean.ParserDescr.cat `term 51))

def EuclidGeom.perpendicularNotation : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def EuclidGeom.perpendicularNotationImpl : Lean.Macro

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem EuclidGeom.Perpendicular.irrefl {α : Type u_2} [EuclidGeom.ProjObj α] (l : α) : ¬EuclidGeom.Perpendicular l l

A projective object $l$ is not perpendicular to itself.

theorem EuclidGeom.Perpendicular.symm {α : Type u_2} {β : Type u_3} [EuclidGeom.ProjObj α] [EuclidGeom.ProjObj β] {l₁ : α} {l₂ : β} (h : EuclidGeom.Perpendicular l₁ l₂) : EuclidGeom.Perpendicular l₂ l₁

theorem EuclidGeom.parallel_of_perp_perp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [EuclidGeom.ProjObj α] [EuclidGeom.ProjObj β] [EuclidGeom.ProjObj γ] {l₁ : α} {l₂ : β} {l₃ : γ} (h₁ : EuclidGeom.Perpendicular l₁ l₂) (h₂ : EuclidGeom.Perpendicular l₂ l₃) : EuclidGeom.Parallel l₁ l₃

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 EuclidGeom.perp_of_parallel_perp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [EuclidGeom.ProjObj α] [EuclidGeom.ProjObj β] [EuclidGeom.ProjObj γ] {l₁ : α} {l₂ : β} {l₃ : γ} (h₁ : EuclidGeom.Parallel l₁ l₂) (h₂ : EuclidGeom.Perpendicular l₂ l₃) : EuclidGeom.Perpendicular l₁ l₃

theorem EuclidGeom.Parallel.trans_perp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [EuclidGeom.ProjObj α] [EuclidGeom.ProjObj β] [EuclidGeom.ProjObj γ] {l₁ : α} {l₂ : β} {l₃ : γ} (h₁ : EuclidGeom.Parallel l₁ l₂) (h₂ : EuclidGeom.Perpendicular l₂ l₃) : EuclidGeom.Perpendicular l₁ l₃

Alias of EuclidGeom.perp_of_parallel_perp.

theorem EuclidGeom.perp_of_perp_parallel {α : Type u_2} {β : Type u_3} {γ : Type u_4} [EuclidGeom.ProjObj α] [EuclidGeom.ProjObj β] [EuclidGeom.ProjObj γ] {l₁ : α} {l₂ : β} {l₃ : γ} (h₁ : EuclidGeom.Perpendicular l₁ l₂) (h₂ : EuclidGeom.Parallel l₂ l₃) : EuclidGeom.Perpendicular l₁ l₃

theorem EuclidGeom.toProj_ne_toProj_of_perp {α : Type u_2} {β : Type u_3} [EuclidGeom.ProjObj α] [EuclidGeom.ProjObj β] {l₁ : α} {l₂ : β} (h : EuclidGeom.Perpendicular l₁ l₂) : EuclidGeom.toProj l₁ ≠ EuclidGeom.toProj l₂

If $l_1$ is perpendicular to $l_2$, then they have different projective direction.

theorem EuclidGeom.not_parallel_of_perp {α : Type u_2} {β : Type u_3} [EuclidGeom.ProjObj α] [EuclidGeom.ProjObj β] {l₁ : α} {l₂ : β} (h : EuclidGeom.Perpendicular l₁ l₂) : ¬EuclidGeom.Parallel l₁ l₂

def EuclidGeom.perp_line {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (l : EuclidGeom.Line P) : EuclidGeom.Line P

Given a point $A$ and a line $l$, this function returns the line through $A$ perpendicular to $l$.

Equations

• EuclidGeom.perp_line A l = EuclidGeom.Line.mk_pt_proj A l.toProj.perp

@[simp]

theorem EuclidGeom.toProj_of_perp_line_eq_toProj_perp {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (l : EuclidGeom.Line P) : (EuclidGeom.perp_line A l).toProj = l.toProj.perp

theorem EuclidGeom.perp_line_perp {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (l : EuclidGeom.Line P) : EuclidGeom.Perpendicular (EuclidGeom.perp_line A l) l

For a point $A$ and a line $l$, the line through $A$ perpendicular to $l$ constructed using perp_line is perpendicular to $l$.

theorem EuclidGeom.toProj_ne_perp_toProj {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (l : EuclidGeom.Line P) : l.toProj ≠ (EuclidGeom.perp_line A l).toProj

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

def EuclidGeom.perp_foot {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (l : EuclidGeom.Line P) : P

For a point $A$ and a line $l$, this function returns the perpendicular foot from $A$ to $l$.

Equations

• EuclidGeom.perp_foot A l = EuclidGeom.Line.inx l (EuclidGeom.perp_line A l) (_ : l.toProj ≠ (EuclidGeom.perp_line A l).toProj)

theorem EuclidGeom.perp_foot_lies_on_line {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (l : EuclidGeom.Line P) : EuclidGeom.lies_on (EuclidGeom.perp_foot A l) l

theorem EuclidGeom.perp_foot_eq_self_iff_lies_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (l : EuclidGeom.Line P) : EuclidGeom.perp_foot A l = A ↔ EuclidGeom.lies_on A l

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 EuclidGeom.perp_foot_ne_self_iff_not_lies_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (l : EuclidGeom.Line P) : EuclidGeom.perp_foot A l ≠ A ↔ ¬EuclidGeom.lies_on A l

theorem EuclidGeom.pt_ne_iff_not_lies_on_of_eq_perp_foot {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {l : EuclidGeom.Line P} (h : B = EuclidGeom.perp_foot A l) : B ≠ A ↔ ¬EuclidGeom.lies_on A l

theorem EuclidGeom.line_of_self_perp_foot_eq_perp_line_of_not_lies_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {l : EuclidGeom.Line P} (h : ¬EuclidGeom.lies_on A l) : LIN A (EuclidGeom.perp_foot A l) (_ : EuclidGeom.perp_foot A l ≠ A) = EuclidGeom.perp_line 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 EuclidGeom.line_of_self_perp_foot_perp_line_of_not_lies_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {l : EuclidGeom.Line P} (h : ¬EuclidGeom.lies_on A l) : EuclidGeom.Perpendicular (LIN A (EuclidGeom.perp_foot A l) (_ : EuclidGeom.perp_foot A l ≠ A)) 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$.

def EuclidGeom.dist_pt_line {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (l : EuclidGeom.Line P) : ℝ

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

Equations

• EuclidGeom.dist_pt_line A l = { source := A, target := EuclidGeom.perp_foot A l }.length

theorem EuclidGeom.dist_eq_zero_iff_lies_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (l : EuclidGeom.Line P) : EuclidGeom.dist_pt_line A l = 0 ↔ EuclidGeom.lies_on A l

theorem EuclidGeom.perp_foot_unique {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {l : EuclidGeom.Line P} (h : EuclidGeom.lies_on B l) [_hne : EuclidGeom.PtNe A B] (hp : EuclidGeom.Perpendicular (LIN A B) l) : EuclidGeom.perp_foot A l = B

theorem EuclidGeom.perp_foot_unique' {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {l : EuclidGeom.DirLine P} (h : EuclidGeom.lies_on B l) [_hne : EuclidGeom.PtNe A B] (hp : EuclidGeom.Perpendicular (DLIN A B) l) : EuclidGeom.perp_foot A l.toLine = B

theorem EuclidGeom.dist_pt_line_shortest {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) {l : EuclidGeom.Line P} (h : EuclidGeom.lies_on B l) : dist A B ≥ EuclidGeom.dist_pt_line A l

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 EuclidGeom.eq_dist_pt_line_iff_eq_perp_foot {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {l : EuclidGeom.Line P} (h : EuclidGeom.lies_on B l) : dist A B = EuclidGeom.dist_pt_line A l ↔ B = EuclidGeom.perp_foot A l

theorem EuclidGeom.perp_of_inner_product_eq_zero (v : EuclidGeom.VecND) (w : EuclidGeom.VecND) (h : inner ↑v ↑w = 0) : EuclidGeom.Perpendicular v w

theorem EuclidGeom.inner_product_eq_zero_of_perp (v : EuclidGeom.VecND) (w : EuclidGeom.VecND) (h : EuclidGeom.Perpendicular v w) : inner ↑v ↑w = 0

theorem EuclidGeom.perp_iff_inner_eq_zero {v : EuclidGeom.VecND} {w : EuclidGeom.VecND} : EuclidGeom.Perpendicular v w ↔ inner ↑v ↑w = 0

theorem EuclidGeom.inner_vec_pt_pt_vec_pt_perp_foot_eq_inner_vec_pt_perp_foot {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) {l : EuclidGeom.DirLine P} (ha : EuclidGeom.lies_on A l) : inner (EuclidGeom.Vec.mkPtPt A B) (EuclidGeom.Vec.mkPtPt A (EuclidGeom.perp_foot B l.toLine)) = inner (EuclidGeom.Vec.mkPtPt A (EuclidGeom.perp_foot B l.toLine)) (EuclidGeom.Vec.mkPtPt A (EuclidGeom.perp_foot B l.toLine))

theorem EuclidGeom.inner_vec_pt_pt_dirLine_toDir_unitVec_eq_inner_vec_pt_perp_foot {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) {l : EuclidGeom.DirLine P} (ha : EuclidGeom.lies_on A l) : inner (EuclidGeom.Vec.mkPtPt A B) l.toDir.unitVec = inner (EuclidGeom.Vec.mkPtPt A (EuclidGeom.perp_foot B l.toLine)) l.toDir.unitVec

theorem EuclidGeom.inner_eq_ddist_pt_perp_foot {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) {l : EuclidGeom.DirLine P} (ha : EuclidGeom.lies_on A l) : inner (EuclidGeom.Vec.mkPtPt A B) l.toDir.unitVec = EuclidGeom.DirLine.ddist ha (_ : EuclidGeom.lies_on (EuclidGeom.perp_foot B l.toLine) l.toLine)

theorem EuclidGeom.perp_foot_eq_inner_smul_toDir_unitVec_vadd {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) {l : EuclidGeom.DirLine P} (ha : EuclidGeom.lies_on A l) : EuclidGeom.perp_foot B l.toLine = inner (EuclidGeom.Vec.mkPtPt A B) l.toDir.unitVec • l.toDir.unitVec +ᵥ A

theorem EuclidGeom.vec_pt_perp_foot_eq_ddist_smul_toDir_unitVec {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) {l : EuclidGeom.DirLine P} (ha : EuclidGeom.lies_on A l) : EuclidGeom.Vec.mkPtPt A (EuclidGeom.perp_foot B l.toLine) = inner (EuclidGeom.Vec.mkPtPt A B) l.toDir.unitVec • l.toDir.unitVec

theorem EuclidGeom.inner_vec_pt_pt_vec_pt_perp_foot_eq_dist_sq {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) {l : EuclidGeom.DirLine P} (ha : EuclidGeom.lies_on A l) : inner (EuclidGeom.Vec.mkPtPt A B) (EuclidGeom.Vec.mkPtPt A (EuclidGeom.perp_foot B l.toLine)) = dist A (EuclidGeom.perp_foot B l.toLine) ^ 2

theorem EuclidGeom.inner_vec_pt_pt_vec_perp_foot_perp_foot_eq_inner_vec_perp_foot_perp_foot {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) {l : EuclidGeom.DirLine P} : inner (EuclidGeom.Vec.mkPtPt A B) (EuclidGeom.Vec.mkPtPt (EuclidGeom.perp_foot A l.toLine) (EuclidGeom.perp_foot B l.toLine)) = inner (EuclidGeom.Vec.mkPtPt (EuclidGeom.perp_foot A l.toLine) (EuclidGeom.perp_foot B l.toLine)) (EuclidGeom.Vec.mkPtPt (EuclidGeom.perp_foot A l.toLine) (EuclidGeom.perp_foot B l.toLine))

theorem EuclidGeom.inner_vec_pt_pt_dirLine_toDir_unitVec_eq_inner_vec_perp_foot_perp_foot {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) {l : EuclidGeom.DirLine P} : inner (EuclidGeom.Vec.mkPtPt A B) l.toDir.unitVec = inner (EuclidGeom.Vec.mkPtPt (EuclidGeom.perp_foot A l.toLine) (EuclidGeom.perp_foot B l.toLine)) l.toDir.unitVec

theorem EuclidGeom.inner_eq_ddist_perp_foot_perp_foot {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) {l : EuclidGeom.DirLine P} : inner (EuclidGeom.Vec.mkPtPt A B) l.toDir.unitVec = EuclidGeom.DirLine.ddist (_ : EuclidGeom.lies_on (EuclidGeom.perp_foot A l.toLine) l.toLine) (_ : EuclidGeom.lies_on (EuclidGeom.perp_foot B l.toLine) l.toLine)

theorem EuclidGeom.perp_foot_eq_inner_smul_toDir_unitVec_vadd_perp_foot {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) {l : EuclidGeom.DirLine P} : EuclidGeom.perp_foot B l.toLine = inner (EuclidGeom.Vec.mkPtPt A B) l.toDir.unitVec • l.toDir.unitVec +ᵥ EuclidGeom.perp_foot A l.toLine

theorem EuclidGeom.vec_perp_foot_perp_foot_eq_ddist_smul_toDir_unitVec {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) {l : EuclidGeom.DirLine P} : EuclidGeom.Vec.mkPtPt (EuclidGeom.perp_foot A l.toLine) (EuclidGeom.perp_foot B l.toLine) = inner (EuclidGeom.Vec.mkPtPt A B) l.toDir.unitVec • l.toDir.unitVec

theorem EuclidGeom.inner_vec_pt_pt_vec_perp_foot_perp_foot_eq_dist_sq {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) {l : EuclidGeom.DirLine P} : inner (EuclidGeom.Vec.mkPtPt A B) (EuclidGeom.Vec.mkPtPt (EuclidGeom.perp_foot A l.toLine) (EuclidGeom.perp_foot B l.toLine)) = dist (EuclidGeom.perp_foot A l.toLine) (EuclidGeom.perp_foot B l.toLine) ^ 2