EuclideanGeometry.Foundation.Axiom.Circle.CirclePower

def EuclidGeom.Circle.power {P : Type u_1} [EuclidGeom.EuclideanPlane P] (ω : EuclidGeom.Circle P) (p : P) :

Equations

EuclidGeom.Circle.power ω p = dist ω.center p ^ 2 - ω.radius ^ 2

Instances For

theorem EuclidGeom.Circle.pt_liesin_circle_iff_power_npos {P : Type u_1} [EuclidGeom.EuclideanPlane P] (p : P) (ω : EuclidGeom.Circle P) :

EuclidGeom.Circle.IsInside p ω ↔ EuclidGeom.Circle.power ω p ≤ 0

source

theorem EuclidGeom.Circle.pt_liesint_circle_iff_power_neg {P : Type u_1} [EuclidGeom.EuclideanPlane P] (p : P) (ω : EuclidGeom.Circle P) :

EuclidGeom.lies_int p ω ↔ EuclidGeom.Circle.power ω p < 0

source

theorem EuclidGeom.Circle.pt_lieson_circle_iff_power_zero {P : Type u_1} [EuclidGeom.EuclideanPlane P] (p : P) (ω : EuclidGeom.Circle P) :

EuclidGeom.lies_on p ω ↔ EuclidGeom.Circle.power ω p = 0

source

theorem EuclidGeom.Circle.pt_liesout_circle_iff_power_pos {P : Type u_1} [EuclidGeom.EuclideanPlane P] (p : P) (ω : EuclidGeom.Circle P) :

EuclidGeom.Circle.IsOutside p ω ↔ 0 < EuclidGeom.Circle.power ω p

source

theorem EuclidGeom.Circle.Tangents.ext_iff {P : Type u_2} :

∀ {inst : EuclidGeom.EuclideanPlane P} (x y : EuclidGeom.Circle.Tangents P), x = y ↔ x.left = y.left ∧ x.right = y.right

source

theorem EuclidGeom.Circle.Tangents.ext {P : Type u_2} :

∀ {inst : EuclidGeom.EuclideanPlane P} (x y : EuclidGeom.Circle.Tangents P), x.left = y.left → x.right = y.right → x = y

source

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

Type u_2

left : P
right : P

Instances For

source

theorem EuclidGeom.Circle.tangent_circle_intersected {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} {p : P} (h : EuclidGeom.Circle.IsOutside p ω) :

EuclidGeom.Circle.CC.IsIntersected (EuclidGeom.Circle.mk_pt_pt_diam p ω.center) ω

source

def EuclidGeom.Circle.pt_outside_tangent_pts {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} {p : P} (h : EuclidGeom.Circle.IsOutside p ω) :

EuclidGeom.Circle.Tangents P

Equations

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

Instances For

source

theorem EuclidGeom.Circle.tangents_lieson_circle {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} {p : P} (h : EuclidGeom.Circle.IsOutside p ω) :

EuclidGeom.lies_on (EuclidGeom.Circle.pt_outside_tangent_pts h).left ω ∧ EuclidGeom.lies_on (EuclidGeom.Circle.pt_outside_tangent_pts h).right ω

source

theorem EuclidGeom.Circle.tangents_ne_pt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} {p : P} (h : EuclidGeom.Circle.IsOutside p ω) :

(EuclidGeom.Circle.pt_outside_tangent_pts h).left ≠ p ∧ (EuclidGeom.Circle.pt_outside_tangent_pts h).right ≠ p

source

theorem EuclidGeom.Circle.tangents_ne_center {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} {p : P} (h : EuclidGeom.Circle.IsOutside p ω) :

(EuclidGeom.Circle.pt_outside_tangent_pts h).left ≠ ω.center ∧ (EuclidGeom.Circle.pt_outside_tangent_pts h).right ≠ ω.center

source

theorem EuclidGeom.Circle.tangents_perp₁ {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} {p : P} (h : EuclidGeom.Circle.IsOutside p ω) :

EuclidGeom.Perpendicular (DLIN p (EuclidGeom.Circle.pt_outside_tangent_pts h).left (_ : (EuclidGeom.Circle.pt_outside_tangent_pts h).left ≠ p)) (DLIN ω.center (EuclidGeom.Circle.pt_outside_tangent_pts h).left (_ : (EuclidGeom.Circle.pt_outside_tangent_pts h).left ≠ ω.center))

source

theorem EuclidGeom.Circle.tangents_perp₂ {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} {p : P} (h : EuclidGeom.Circle.IsOutside p ω) :

EuclidGeom.Perpendicular (DLIN p (EuclidGeom.Circle.pt_outside_tangent_pts h).right (_ : (EuclidGeom.Circle.pt_outside_tangent_pts h).right ≠ p)) (DLIN ω.center (EuclidGeom.Circle.pt_outside_tangent_pts h).right (_ : (EuclidGeom.Circle.pt_outside_tangent_pts h).right ≠ ω.center))

source

theorem EuclidGeom.Circle.line_tangent_circle {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} {p : P} (h : EuclidGeom.Circle.IsOutside p ω) :

EuclidGeom.Circle.DirLine.IsTangent (DLIN p (EuclidGeom.Circle.pt_outside_tangent_pts h).left (_ : (EuclidGeom.Circle.pt_outside_tangent_pts h).left ≠ p)) ω ∧ EuclidGeom.Circle.DirLine.IsTangent (DLIN p (EuclidGeom.Circle.pt_outside_tangent_pts h).right (_ : (EuclidGeom.Circle.pt_outside_tangent_pts h).right ≠ p)) ω

source

theorem EuclidGeom.Circle.tangent_pts_eq_tangents {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} {p : P} (h : EuclidGeom.Circle.IsOutside p ω) :

EuclidGeom.DirLC.Tangentpt (_ : EuclidGeom.Circle.DirLine.IsTangent (DLIN p (EuclidGeom.Circle.pt_outside_tangent_pts h).left (_ : (EuclidGeom.Circle.pt_outside_tangent_pts h).left ≠ p)) ω) = (EuclidGeom.Circle.pt_outside_tangent_pts h).left ∧ EuclidGeom.DirLC.Tangentpt (_ : EuclidGeom.Circle.DirLine.IsTangent (DLIN p (EuclidGeom.Circle.pt_outside_tangent_pts h).right (_ : (EuclidGeom.Circle.pt_outside_tangent_pts h).right ≠ p)) ω) = (EuclidGeom.Circle.pt_outside_tangent_pts h).right

source

theorem EuclidGeom.Circle.tangent_length_sq_eq_power {P : Type u_1} [EuclidGeom.EuclideanPlane P] {p : P} {l : EuclidGeom.DirLine P} {ω : EuclidGeom.Circle P} (h₁ : EuclidGeom.Circle.DirLine.IsTangent l ω) (h₂ : EuclidGeom.lies_on p l) :

dist p (EuclidGeom.DirLC.Tangentpt h₁) ^ 2 = EuclidGeom.Circle.power ω p

source

theorem EuclidGeom.Circle.tangent_length_sq_eq_power' {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} {A : P} {B : P} (ha : EuclidGeom.Circle.IsOutside A ω) (hb : EuclidGeom.lies_on B ω) (h : EuclidGeom.Circle.DirLine.IsTangent (DLIN A B (_ : B ≠ A)) ω) :

dist A B ^ 2 = EuclidGeom.Circle.power ω A

source

theorem EuclidGeom.Circle.length_of_tangent_eq {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} {p : P} (h : EuclidGeom.Circle.IsOutside p ω) :

dist p (EuclidGeom.Circle.pt_outside_tangent_pts h).left = dist p (EuclidGeom.Circle.pt_outside_tangent_pts h).right

source

theorem EuclidGeom.Circle.length_of_tangent_eq' {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} {A : P} {B : P} {C : P} (ha : EuclidGeom.Circle.IsOutside A ω) (hb : EuclidGeom.lies_on B ω) (hc : EuclidGeom.lies_on C ω) (ht₁ : EuclidGeom.Circle.DirLine.IsTangent (DLIN A B (_ : B ≠ A)) ω) (ht₂ : EuclidGeom.Circle.DirLine.IsTangent (DLIN A C (_ : C ≠ A)) ω) :

dist A B = dist A C

source

theorem EuclidGeom.Circle.pt_liesout_ne_inxpts {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} {p : P} {l : EuclidGeom.DirLine P} (h₁ : EuclidGeom.Circle.DirLine.IsIntersected l ω) (_h₂ : EuclidGeom.lies_on p l) (h₃ : EuclidGeom.Circle.IsOutside p ω) :

p ≠ (EuclidGeom.DirLC.Inxpts h₁).front ∧ p ≠ (EuclidGeom.DirLC.Inxpts h₁).back

source

theorem EuclidGeom.Circle.pt_liesint_ne_inxpts {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} {p : P} {l : EuclidGeom.DirLine P} (h₁ : EuclidGeom.Circle.DirLine.IsIntersected l ω) (_h₂ : EuclidGeom.lies_on p l) (h₃ : EuclidGeom.lies_int p ω) :

p ≠ (EuclidGeom.DirLC.Inxpts h₁).front ∧ p ≠ (EuclidGeom.DirLC.Inxpts h₁).back

source

theorem EuclidGeom.Circle.pt_liesout_back_lieson_ray_pt_front {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} {p : P} {l : EuclidGeom.DirLine P} (h₁ : EuclidGeom.Circle.DirLine.IsIntersected l ω) (h₂ : EuclidGeom.lies_on p l) (h₃ : EuclidGeom.Circle.IsOutside p ω) :

EuclidGeom.lies_on (EuclidGeom.DirLC.Inxpts h₁).back (RAY p (EuclidGeom.DirLC.Inxpts h₁).front (_ : (EuclidGeom.DirLC.Inxpts h₁).front ≠ p))

source

theorem EuclidGeom.Circle.pt_liesint_back_lieson_ray_pt_front_reverse {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} {p : P} {l : EuclidGeom.DirLine P} (h₁ : EuclidGeom.Circle.DirLine.IsIntersected l ω) (h₂ : EuclidGeom.lies_on p l) (h₃ : EuclidGeom.lies_int p ω) :

EuclidGeom.lies_on (EuclidGeom.DirLC.Inxpts h₁).back (RAY p (EuclidGeom.DirLC.Inxpts h₁).front (_ : (EuclidGeom.DirLC.Inxpts h₁).front ≠ p)).reverse

source

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

inner (EuclidGeom.Vec.mkPtPt p (EuclidGeom.DirLC.Inxpts h₁).front) (EuclidGeom.Vec.mkPtPt p (EuclidGeom.DirLC.Inxpts h₁).back) = EuclidGeom.Circle.power ω p

source

theorem EuclidGeom.Circle.chord_power_thm {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} {p : P} {l : EuclidGeom.DirLine P} (h₁ : EuclidGeom.Circle.DirLine.IsIntersected l ω) (h₂ : EuclidGeom.lies_on p l) (h₃ : EuclidGeom.lies_int p ω) :

dist p (EuclidGeom.DirLC.Inxpts h₁).front * dist p (EuclidGeom.DirLC.Inxpts h₁).back = -EuclidGeom.Circle.power ω p

source

theorem EuclidGeom.Circle.secant_power_thm {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} {p : P} {l : EuclidGeom.DirLine P} (h₁ : EuclidGeom.Circle.DirLine.IsIntersected l ω) (h₂ : EuclidGeom.lies_on p l) (h₃ : EuclidGeom.Circle.IsOutside p ω) :

dist p (EuclidGeom.DirLC.Inxpts h₁).front * dist p (EuclidGeom.DirLC.Inxpts h₁).back = EuclidGeom.Circle.power ω p

source

theorem EuclidGeom.Circle.intersecting_chords_thm {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} {S : P} {s₁ : EuclidGeom.Chord P ω} {s₂ : EuclidGeom.Chord P ω} (h : EuclidGeom.lies_int S ω) (h₁ : EuclidGeom.lies_on S s₁) (h₂ : EuclidGeom.lies_on S s₂) :

dist S s₁.toSegND.source * dist S s₁.toSegND.target = dist S s₂.toSegND.source * dist S s₂.toSegND.target

source

theorem EuclidGeom.Circle.intersecting_secants_thm {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} {S : P} {l₁ : EuclidGeom.DirLine P} {l₂ : EuclidGeom.DirLine P} (h : EuclidGeom.Circle.IsOutside S ω) (h₁ : EuclidGeom.lies_on S l₁) (h₂ : EuclidGeom.lies_on S l₂) (hx₁ : EuclidGeom.Circle.DirLine.IsIntersected l₁ ω) (hx₂ : EuclidGeom.Circle.DirLine.IsIntersected l₂ ω) :

dist S (EuclidGeom.DirLC.Inxpts hx₁).front * dist S (EuclidGeom.DirLC.Inxpts hx₁).back = dist S (EuclidGeom.DirLC.Inxpts hx₂).front * dist S (EuclidGeom.DirLC.Inxpts hx₂).back