Documentation

EuclideanGeometry.Foundation.Axiom.Circle.LCPosition

def EuclidGeom.Circle.DirLine.IsDisjoint {P : Type u_1} [EuclidGeom.EuclideanPlane P] (l : EuclidGeom.DirLine P) (ω : EuclidGeom.Circle P) :

Equations

EuclidGeom.Circle.DirLine.IsDisjoint l ω = (EuclidGeom.dist_pt_line ω.center l.toLine > ω.radius)

Instances For

def EuclidGeom.Circle.DirLine.IsTangent {P : Type u_1} [EuclidGeom.EuclideanPlane P] (l : EuclidGeom.DirLine P) (ω : EuclidGeom.Circle P) :

Equations

EuclidGeom.Circle.DirLine.IsTangent l ω = (EuclidGeom.dist_pt_line ω.center l.toLine = ω.radius)

Instances For

def EuclidGeom.Circle.DirLine.IsSecant {P : Type u_1} [EuclidGeom.EuclideanPlane P] (l : EuclidGeom.DirLine P) (ω : EuclidGeom.Circle P) :

Equations

EuclidGeom.Circle.DirLine.IsSecant l ω = (EuclidGeom.dist_pt_line ω.center l.toLine < ω.radius)

Instances For

def EuclidGeom.Circle.DirLine.IsIntersected {P : Type u_1} [EuclidGeom.EuclideanPlane P] (l : EuclidGeom.DirLine P) (ω : EuclidGeom.Circle P) :

Equations

EuclidGeom.Circle.DirLine.IsIntersected l ω = (EuclidGeom.dist_pt_line ω.center l.toLine ≤ ω.radius)

Instances For

def EuclidGeom.term_Secant_ :

Lean.TrailingParserDescr

Equations

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

Instances For

def EuclidGeom.term_Tangent_ :

Lean.TrailingParserDescr

Equations

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

Instances For

def EuclidGeom.term_Disjoint_ :

Lean.TrailingParserDescr

Equations

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

Instances For

theorem EuclidGeom.DirLC.disjoint_pt_liesout_circle {P : Type u_1} [EuclidGeom.EuclideanPlane P] {l : EuclidGeom.DirLine P} {ω : EuclidGeom.Circle P} {A : P} (h : EuclidGeom.Circle.DirLine.IsDisjoint l ω) (hh : EuclidGeom.lies_on A l.toLine) :

EuclidGeom.Circle.IsOutside A ω

theorem EuclidGeom.DirLC.intersect_iff_tangent_or_secant {P : Type u_1} [EuclidGeom.EuclideanPlane P] {l : EuclidGeom.DirLine P} {ω : EuclidGeom.Circle P} :

EuclidGeom.Circle.DirLine.IsIntersected l ω ↔ EuclidGeom.Circle.DirLine.IsTangent l ω ∨ EuclidGeom.Circle.DirLine.IsSecant l ω

theorem EuclidGeom.DirLC.pt_liesint_secant {P : Type u_1} [EuclidGeom.EuclideanPlane P] {l : EuclidGeom.DirLine P} {ω : EuclidGeom.Circle P} {A : P} (h₁ : EuclidGeom.lies_int A ω) (h₂ : EuclidGeom.lies_on A l) :

EuclidGeom.Circle.DirLine.IsSecant l ω

theorem EuclidGeom.DirLC.pt_liesint_intersect {P : Type u_1} [EuclidGeom.EuclideanPlane P] {l : EuclidGeom.DirLine P} {ω : EuclidGeom.Circle P} {A : P} (h₁ : EuclidGeom.lies_int A ω) (h₂ : EuclidGeom.lies_on A l) :

EuclidGeom.Circle.DirLine.IsIntersected l ω

theorem EuclidGeom.DirLCInxpts.ext_iff {P : Type u_2} :

∀ {inst : EuclidGeom.EuclideanPlane P} (x y : EuclidGeom.DirLCInxpts P), x = y ↔ x.front = y.front ∧ x.back = y.back

theorem EuclidGeom.DirLCInxpts.ext {P : Type u_2} :

∀ {inst : EuclidGeom.EuclideanPlane P} (x y : EuclidGeom.DirLCInxpts P), x.front = y.front → x.back = y.back → x = y

structure EuclidGeom.DirLCInxpts (P : Type u_2) [EuclidGeom.EuclideanPlane P] :

Type u_2

front : P
back : P

Instances For

theorem EuclidGeom.DirLC.dist_pt_line_ineq {P : Type u_1} [EuclidGeom.EuclideanPlane P] {l : EuclidGeom.DirLine P} {ω : EuclidGeom.Circle P} (h : EuclidGeom.Circle.DirLine.IsIntersected l ω) :

ω.radius ^ 2 - EuclidGeom.dist_pt_line ω.center l.toLine ^ 2 ≥ 0

def EuclidGeom.DirLC.Inxpts {P : Type u_1} [EuclidGeom.EuclideanPlane P] {l : EuclidGeom.DirLine P} {ω : EuclidGeom.Circle P} (_h : EuclidGeom.Circle.DirLine.IsIntersected l ω) :

EuclidGeom.DirLCInxpts P

Equations

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

Instances For

theorem EuclidGeom.DirLC.inx_pts_lieson_dlin {P : Type u_1} [EuclidGeom.EuclideanPlane P] {l : EuclidGeom.DirLine P} {ω : EuclidGeom.Circle P} (h : EuclidGeom.Circle.DirLine.IsIntersected l ω) :

EuclidGeom.lies_on (EuclidGeom.DirLC.Inxpts h).front l ∧ EuclidGeom.lies_on (EuclidGeom.DirLC.Inxpts h).back l

theorem EuclidGeom.DirLC.inx_pts_lieson_circle {P : Type u_1} [EuclidGeom.EuclideanPlane P] {l : EuclidGeom.DirLine P} {ω : EuclidGeom.Circle P} (h : EuclidGeom.Circle.DirLine.IsIntersected l ω) :

EuclidGeom.lies_on (EuclidGeom.DirLC.Inxpts h).front ω ∧ EuclidGeom.lies_on (EuclidGeom.DirLC.Inxpts h).back ω

theorem EuclidGeom.DirLC.inx_pts_same_iff_tangent {P : Type u_1} [EuclidGeom.EuclideanPlane P] {l : EuclidGeom.DirLine P} {ω : EuclidGeom.Circle P} (h : EuclidGeom.Circle.DirLine.IsIntersected l ω) :

(EuclidGeom.DirLC.Inxpts h).back = (EuclidGeom.DirLC.Inxpts h).front ↔ EuclidGeom.Circle.DirLine.IsTangent l ω

theorem EuclidGeom.DirLC.inx_pts_ne_center {P : Type u_1} [EuclidGeom.EuclideanPlane P] {l : EuclidGeom.DirLine P} {ω : EuclidGeom.Circle P} (h : EuclidGeom.Circle.DirLine.IsIntersected l ω) :

(EuclidGeom.DirLC.Inxpts h).front ≠ ω.center ∧ (EuclidGeom.DirLC.Inxpts h).back ≠ ω.center

theorem EuclidGeom.DirLC.inx_pts_antipode_iff_center_lieson {P : Type u_1} [EuclidGeom.EuclideanPlane P] {l : EuclidGeom.DirLine P} {ω : EuclidGeom.Circle P} (h : EuclidGeom.Circle.DirLine.IsIntersected l ω) :

EuclidGeom.Circle.IsAntipode ω (_ : EuclidGeom.lies_on (EuclidGeom.DirLC.Inxpts h).front ω) (_ : EuclidGeom.lies_on (EuclidGeom.DirLC.Inxpts h).back ω) ↔ EuclidGeom.lies_on ω.center l

theorem EuclidGeom.DirLC.inxwith_iff_intersect {P : Type u_1} [EuclidGeom.EuclideanPlane P] {l : EuclidGeom.DirLine P} {ω : EuclidGeom.Circle P} :

EuclidGeom.intersect l ω ↔ EuclidGeom.Circle.DirLine.IsIntersected l ω

theorem EuclidGeom.DirLC.inxwith_iff_tangent_or_secant {P : Type u_1} [EuclidGeom.EuclideanPlane P] {l : EuclidGeom.DirLine P} {ω : EuclidGeom.Circle P} :

EuclidGeom.intersect l ω ↔ EuclidGeom.Circle.DirLine.IsTangent l ω ∨ EuclidGeom.Circle.DirLine.IsSecant l ω

def EuclidGeom.DirLC.Tangentpt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {l : EuclidGeom.DirLine P} {ω : EuclidGeom.Circle P} (h : EuclidGeom.Circle.DirLine.IsTangent l ω) :

P

Equations

EuclidGeom.DirLC.Tangentpt h = (EuclidGeom.DirLC.Inxpts (_ : EuclidGeom.Circle.DirLine.IsIntersected l ω)).front

Instances For

theorem EuclidGeom.DirLC.tangent_pt_ne_center {P : Type u_1} [EuclidGeom.EuclideanPlane P] {l : EuclidGeom.DirLine P} {ω : EuclidGeom.Circle P} (h : EuclidGeom.Circle.DirLine.IsTangent l ω) :

EuclidGeom.DirLC.Tangentpt h ≠ ω.center

theorem EuclidGeom.DirLC.tangent_pt_center_perp_line {P : Type u_1} [EuclidGeom.EuclideanPlane P] {l : EuclidGeom.DirLine P} {ω : EuclidGeom.Circle P} (h : EuclidGeom.Circle.DirLine.IsTangent l ω) :

EuclidGeom.Perpendicular (LIN ω.center (EuclidGeom.DirLC.Tangentpt h) (_ : EuclidGeom.DirLC.Tangentpt h ≠ ω.center)) l.toLine

theorem EuclidGeom.DirLC.tangent_pt_eq_perp_foot {P : Type u_1} [EuclidGeom.EuclideanPlane P] {l : EuclidGeom.DirLine P} {ω : EuclidGeom.Circle P} (h : EuclidGeom.Circle.DirLine.IsTangent l ω) :

EuclidGeom.DirLC.Tangentpt h = EuclidGeom.perp_foot ω.center l.toLine

theorem EuclidGeom.Circle.DirLC_intersection_eq_inxpts {P : Type u_1} [EuclidGeom.EuclideanPlane P] {l : EuclidGeom.DirLine P} {ω : EuclidGeom.Circle P} {A : P} (h : EuclidGeom.Circle.DirLine.IsIntersected l ω) (h₁ : EuclidGeom.lies_on A l.toLine) (h₂ : EuclidGeom.lies_on A ω) :

A = (EuclidGeom.DirLC.Inxpts h).front ∨ A = (EuclidGeom.DirLC.Inxpts h).back

theorem EuclidGeom.Circle.pt_pt_tangent_eq_tangent_pt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {ω : EuclidGeom.Circle P} (h₁ : EuclidGeom.Circle.IsOutside A ω) (h₂ : EuclidGeom.lies_on B ω) (ht : EuclidGeom.Circle.DirLine.IsTangent (DLIN A B (_ : B ≠ A)) ω) :

B = EuclidGeom.DirLC.Tangentpt ht

theorem EuclidGeom.Circle.chord_toDirLine_intersected {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} (s : EuclidGeom.Chord P ω) :

EuclidGeom.Circle.DirLine.IsIntersected s.toSegND.toDirLine ω

theorem EuclidGeom.Circle.chord_toDirLine_inx_front_pt_eq_target {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} (s : EuclidGeom.Chord P ω) :

(EuclidGeom.DirLC.Inxpts (_ : EuclidGeom.Circle.DirLine.IsIntersected s.toSegND.toDirLine ω)).front = s.toSegND.target

theorem EuclidGeom.Circle.chord_toDirLine_inx_back_pt_eq_source {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} (s : EuclidGeom.Chord P ω) :

(EuclidGeom.DirLC.Inxpts (_ : EuclidGeom.Circle.DirLine.IsIntersected s.toSegND.toDirLine ω)).back = s.toSegND.source

theorem EuclidGeom.Circle.pt_pt_tangent_perp {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {ω : EuclidGeom.Circle P} (h₁ : EuclidGeom.Circle.IsOutside A ω) (h₂ : EuclidGeom.lies_on B ω) (ht : EuclidGeom.Circle.DirLine.IsTangent (DLIN A B (_ : B ≠ A)) ω) :

EuclidGeom.Perpendicular (DLIN ω.center B) (DLIN A B (_ : B ≠ A))

theorem EuclidGeom.Circle.pt_pt_perp_tangent {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {ω : EuclidGeom.Circle P} (h₁ : EuclidGeom.Circle.IsOutside A ω) (h₂ : EuclidGeom.lies_on B ω) (hp : EuclidGeom.Perpendicular (DLIN A B (_ : B ≠ A)) (DLIN ω.center B)) :

EuclidGeom.Circle.DirLine.IsTangent (DLIN A B (_ : B ≠ A)) ω

theorem EuclidGeom.Circle.pt_pt_perp_eq_tangent_pt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {ω : EuclidGeom.Circle P} (h₁ : EuclidGeom.Circle.IsOutside A ω) (h₂ : EuclidGeom.lies_on B ω) (hp : EuclidGeom.Perpendicular (DLIN A B (_ : B ≠ A)) (DLIN ω.center B)) :

B = EuclidGeom.DirLC.Tangentpt (_ : EuclidGeom.Circle.DirLine.IsTangent (DLIN A B (_ : B ≠ A)) ω)

def EuclidGeom.Circle.Line.IsDisjoint {P : Type u_1} [EuclidGeom.EuclideanPlane P] (l : EuclidGeom.Line P) (ω : EuclidGeom.Circle P) :

Equations

EuclidGeom.Circle.Line.IsDisjoint l ω = (EuclidGeom.dist_pt_line ω.center l > ω.radius)

Instances For

def EuclidGeom.Circle.Line.IsTangent {P : Type u_1} [EuclidGeom.EuclideanPlane P] (l : EuclidGeom.Line P) (ω : EuclidGeom.Circle P) :

Equations

EuclidGeom.Circle.Line.IsTangent l ω = (EuclidGeom.dist_pt_line ω.center l = ω.radius)

Instances For

def EuclidGeom.Circle.Line.IsSecant {P : Type u_1} [EuclidGeom.EuclideanPlane P] (l : EuclidGeom.Line P) (ω : EuclidGeom.Circle P) :

Equations

EuclidGeom.Circle.Line.IsSecant l ω = (EuclidGeom.dist_pt_line ω.center l < ω.radius)

Instances For

def EuclidGeom.Circle.Line.IsIntersected {P : Type u_1} [EuclidGeom.EuclideanPlane P] (l : EuclidGeom.Line P) (ω : EuclidGeom.Circle P) :

Equations

EuclidGeom.Circle.Line.IsIntersected l ω = (EuclidGeom.dist_pt_line ω.center l ≤ ω.radius)

Instances For