Documentation

EuclideanGeometry.Foundation.Axiom.Circle.CCPosition

def EuclidGeom.Circle.CC.IsSeparated {P : Type u_1} [EuclidGeom.EuclideanPlane P] (ω₁ : EuclidGeom.Circle P) (ω₂ : EuclidGeom.Circle P) :

Equations

EuclidGeom.Circle.CC.IsSeparated ω₁ ω₂ = (dist ω₁.center ω₂.center > ω₁.radius + ω₂.radius)

Instances For

def EuclidGeom.Circle.CC.IsIntersected {P : Type u_1} [EuclidGeom.EuclideanPlane P] (ω₁ : EuclidGeom.Circle P) (ω₂ : EuclidGeom.Circle P) :

Equations

EuclidGeom.Circle.CC.IsIntersected ω₁ ω₂ = (dist ω₁.center ω₂.center < ω₁.radius + ω₂.radius ∧ dist ω₁.center ω₂.center > |ω₂.radius - ω₁.radius|)

Instances For

def EuclidGeom.Circle.CC.IsExtangent {P : Type u_1} [EuclidGeom.EuclideanPlane P] (ω₁ : EuclidGeom.Circle P) (ω₂ : EuclidGeom.Circle P) :

Equations

EuclidGeom.Circle.CC.IsExtangent ω₁ ω₂ = (dist ω₁.center ω₂.center = ω₁.radius + ω₂.radius)

Instances For

def EuclidGeom.Circle.CC.IsIntangent {P : Type u_1} [EuclidGeom.EuclideanPlane P] (ω₁ : EuclidGeom.Circle P) (ω₂ : EuclidGeom.Circle P) :

Equations

EuclidGeom.Circle.CC.IsIntangent ω₁ ω₂ = (dist ω₁.center ω₂.center = ω₂.radius - ω₁.radius ∧ ω₁.center ≠ ω₂.center)

Instances For

def EuclidGeom.Circle.CC.IsIncluded {P : Type u_1} [EuclidGeom.EuclideanPlane P] (ω₁ : EuclidGeom.Circle P) (ω₂ : EuclidGeom.Circle P) :

Equations

EuclidGeom.Circle.CC.IsIncluded ω₁ ω₂ = (dist ω₁.center ω₂.center < ω₂.radius - ω₁.radius)

Instances For

def EuclidGeom.term_Separate_ :

Lean.TrailingParserDescr

Equations

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

Instances For

def EuclidGeom.term_Intersect_ :

Lean.TrailingParserDescr

Equations

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

Instances For

def EuclidGeom.term_Extangent_ :

Lean.TrailingParserDescr

Equations

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

Instances For

def EuclidGeom.term_Intangent_ :

Lean.TrailingParserDescr

Equations

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

Instances For

def EuclidGeom.term_IncludeIn_ :

Lean.TrailingParserDescr

Equations

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

Instances For

theorem EuclidGeom.CC.separate_symm {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω₁ : EuclidGeom.Circle P} {ω₂ : EuclidGeom.Circle P} :

EuclidGeom.Circle.CC.IsSeparated ω₁ ω₂ ↔ EuclidGeom.Circle.CC.IsSeparated ω₂ ω₁

theorem EuclidGeom.CC.separated_pt_liesout_second_circle {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω₁ : EuclidGeom.Circle P} {ω₂ : EuclidGeom.Circle P} {A : P} (h₁ : EuclidGeom.Circle.CC.IsSeparated ω₁ ω₂) (h₂ : EuclidGeom.lies_on A ω₁) :

EuclidGeom.Circle.IsOutside A ω₂

theorem EuclidGeom.CC.separated_pt_liesout_first_circle {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω₁ : EuclidGeom.Circle P} {ω₂ : EuclidGeom.Circle P} {A : P} (h₁ : EuclidGeom.Circle.CC.IsSeparated ω₁ ω₂) (h₂ : EuclidGeom.lies_on A ω₂) :

EuclidGeom.Circle.IsOutside A ω₁

theorem EuclidGeom.CC.extangent_symm {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω₁ : EuclidGeom.Circle P} {ω₂ : EuclidGeom.Circle P} :

EuclidGeom.Circle.CC.IsExtangent ω₁ ω₂ ↔ EuclidGeom.Circle.CC.IsExtangent ω₂ ω₁

theorem EuclidGeom.CC.extangent_centers_distinct {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω₁ : EuclidGeom.Circle P} {ω₂ : EuclidGeom.Circle P} (h : EuclidGeom.Circle.CC.IsExtangent ω₁ ω₂) :

ω₁.center ≠ ω₂.center

def EuclidGeom.CC.Extangentpt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω₁ : EuclidGeom.Circle P} {ω₂ : EuclidGeom.Circle P} (h : EuclidGeom.Circle.CC.IsExtangent ω₁ ω₂) :

P

Equations

EuclidGeom.CC.Extangentpt h = ω₁.radius • (VEC_nd ω₁.center ω₂.center (_ : ω₂.center ≠ ω₁.center)).toDir.unitVec +ᵥ ω₁.center

Instances For

theorem EuclidGeom.CC.extangent_pt_lieson_circles {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω₁ : EuclidGeom.Circle P} {ω₂ : EuclidGeom.Circle P} (h : EuclidGeom.Circle.CC.IsExtangent ω₁ ω₂) :

EuclidGeom.lies_on (EuclidGeom.CC.Extangentpt h) ω₁ ∧ EuclidGeom.lies_on (EuclidGeom.CC.Extangentpt h) ω₂

theorem EuclidGeom.CC.extangent_pt_centers_collinear {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω₁ : EuclidGeom.Circle P} {ω₂ : EuclidGeom.Circle P} (h : EuclidGeom.Circle.CC.IsExtangent ω₁ ω₂) :

EuclidGeom.Collinear ω₁.center (EuclidGeom.CC.Extangentpt h) ω₂.center

theorem EuclidGeom.CC.intangency_pt_liesin_second_circle {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω₁ : EuclidGeom.Circle P} {ω₂ : EuclidGeom.Circle P} {A : P} (h₁ : EuclidGeom.Circle.CC.IsIntangent ω₁ ω₂) (h₂ : EuclidGeom.lies_on A ω₁) :

EuclidGeom.Circle.IsInside A ω₂

def EuclidGeom.CC.Intangentpt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω₁ : EuclidGeom.Circle P} {ω₂ : EuclidGeom.Circle P} (h : EuclidGeom.Circle.CC.IsIntangent ω₁ ω₂) :

P

Equations

EuclidGeom.CC.Intangentpt h = ω₁.radius • (VEC_nd ω₂.center ω₁.center (_ : ω₁.center ≠ ω₂.center)).toDir.unitVec +ᵥ ω₁.center

Instances For

theorem EuclidGeom.CC.intangent_pt_lieson_circles {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω₁ : EuclidGeom.Circle P} {ω₂ : EuclidGeom.Circle P} (h : EuclidGeom.Circle.CC.IsIntangent ω₁ ω₂) :

EuclidGeom.lies_on (EuclidGeom.CC.Intangentpt h) ω₁ ∧ EuclidGeom.lies_on (EuclidGeom.CC.Intangentpt h) ω₂

theorem EuclidGeom.CC.intangentpt_centers_collinear {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω₁ : EuclidGeom.Circle P} {ω₂ : EuclidGeom.Circle P} (h : EuclidGeom.Circle.CC.IsIntangent ω₁ ω₂) :

EuclidGeom.Collinear ω₁.center ω₂.center (EuclidGeom.CC.Intangentpt h)

theorem EuclidGeom.CC.included_pt_liesint_second_circle {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω₁ : EuclidGeom.Circle P} {ω₂ : EuclidGeom.Circle P} {A : P} (h₁ : EuclidGeom.Circle.CC.IsIncluded ω₁ ω₂) (h₂ : EuclidGeom.lies_on A ω₁) :

EuclidGeom.lies_int A ω₂

theorem EuclidGeom.CC.included_pt_liesout_first_circle {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω₁ : EuclidGeom.Circle P} {ω₂ : EuclidGeom.Circle P} {A : P} (h₁ : EuclidGeom.Circle.CC.IsIncluded ω₁ ω₂) (h₂ : EuclidGeom.lies_on A ω₂) :

EuclidGeom.Circle.IsOutside A ω₁

theorem EuclidGeom.CC.intersected_symm {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω₁ : EuclidGeom.Circle P} {ω₂ : EuclidGeom.Circle P} :

EuclidGeom.Circle.CC.IsIntersected ω₁ ω₂ ↔ EuclidGeom.Circle.CC.IsIntersected ω₂ ω₁

theorem EuclidGeom.CC.intersected_centers_distinct {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω₁ : EuclidGeom.Circle P} {ω₂ : EuclidGeom.Circle P} (h : EuclidGeom.Circle.CC.IsIntersected ω₁ ω₂) :

ω₁.center ≠ ω₂.center

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

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

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

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

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

Type u_2

left : P
right : P

Instances For

def EuclidGeom.Circle.radical_axis_dist_to_the_first {P : Type u_1} [EuclidGeom.EuclideanPlane P] (ω₁ : EuclidGeom.Circle P) (ω₂ : EuclidGeom.Circle P) :

Equations

EuclidGeom.Circle.radical_axis_dist_to_the_first ω₁ ω₂ = (ω₁.radius ^ 2 + dist ω₁.center ω₂.center ^ 2 - ω₂.radius ^ 2) / (2 * dist ω₁.center ω₂.center)

Instances For

theorem EuclidGeom.Circle.radical_axis_dist_lt_radius {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω₁ : EuclidGeom.Circle P} {ω₂ : EuclidGeom.Circle P} (h : EuclidGeom.Circle.CC.IsIntersected ω₁ ω₂) :

|EuclidGeom.Circle.radical_axis_dist_to_the_first ω₁ ω₂| < ω₁.radius

def EuclidGeom.CC.Inxpts {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω₁ : EuclidGeom.Circle P} {ω₂ : EuclidGeom.Circle P} (h : EuclidGeom.Circle.CC.IsIntersected ω₁ ω₂) :

EuclidGeom.CCInxpts P

Equations

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

Instances For

theorem EuclidGeom.CC.inx_pts_distinct {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω₁ : EuclidGeom.Circle P} {ω₂ : EuclidGeom.Circle P} (h : EuclidGeom.Circle.CC.IsIntersected ω₁ ω₂) :

(EuclidGeom.CC.Inxpts h).left ≠ (EuclidGeom.CC.Inxpts h).right

theorem EuclidGeom.CC.inx_pts_lieson_circles {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω₁ : EuclidGeom.Circle P} {ω₂ : EuclidGeom.Circle P} (h : EuclidGeom.Circle.CC.IsIntersected ω₁ ω₂) :

EuclidGeom.lies_on (EuclidGeom.CC.Inxpts h).left ω₁ ∧ EuclidGeom.lies_on (EuclidGeom.CC.Inxpts h).left ω₂ ∧ EuclidGeom.lies_on (EuclidGeom.CC.Inxpts h).right ω₁ ∧ EuclidGeom.lies_on (EuclidGeom.CC.Inxpts h).right ω₂

theorem EuclidGeom.CC.inx_pts_not_collinear {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω₁ : EuclidGeom.Circle P} {ω₂ : EuclidGeom.Circle P} (h : EuclidGeom.Circle.CC.IsIntersected ω₁ ω₂) :

¬EuclidGeom.Collinear (EuclidGeom.CC.Inxpts h).left ω₁.center ω₂.center ∧ ¬EuclidGeom.Collinear (EuclidGeom.CC.Inxpts h).right ω₁.center ω₂.center

theorem EuclidGeom.CC.inx_pts_tri_acongr {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω₁ : EuclidGeom.Circle P} {ω₂ : EuclidGeom.Circle P} (h : EuclidGeom.Circle.CC.IsIntersected ω₁ ω₂) :

EuclidGeom.HasACongr.acongr { point₁ := ω₁.center, point₂ := ω₂.center, point₃ := (EuclidGeom.CC.Inxpts h).left } { point₁ := ω₁.center, point₂ := ω₂.center, point₃ := (EuclidGeom.CC.Inxpts h).right }

theorem EuclidGeom.CC.inx_pts_line_perp_center_line {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω₁ : EuclidGeom.Circle P} {ω₂ : EuclidGeom.Circle P} (h : EuclidGeom.Circle.CC.IsIntersected ω₁ ω₂) :

EuclidGeom.Perpendicular (LIN (EuclidGeom.CC.Inxpts h).left (EuclidGeom.CC.Inxpts h).right (_ : (EuclidGeom.CC.Inxpts h).right ≠ (EuclidGeom.CC.Inxpts h).left)) (LIN ω₁.center ω₂.center (_ : ω₂.center ≠ ω₁.center))

theorem EuclidGeom.CC.inx_pts_uniqueness {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω₁ : EuclidGeom.Circle P} {ω₂ : EuclidGeom.Circle P} {A : P} (h : EuclidGeom.Circle.CC.IsIntersected ω₁ ω₂) (h₁ : EuclidGeom.lies_on A ω₁) (h₂ : EuclidGeom.lies_on A ω₂) :

A = (EuclidGeom.CC.Inxpts h).left ∨ A = (EuclidGeom.CC.Inxpts h).right