EuclideanGeometry.Foundation.Axiom.Circle.InscribedAngle

source

def EuclidGeom.Arc.cangle {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} (β : EuclidGeom.Arc P ω) :

EuclidGeom.Angle P

Equations

EuclidGeom.Arc.cangle β = ANG β.source ω.center β.target (_ : β.source ≠ ω.center) (_ : β.target ≠ ω.center)

Instances For

source

def EuclidGeom.Arc.IsMajor {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} (β : EuclidGeom.Arc P ω) :

Prop

Equations

EuclidGeom.Arc.IsMajor β = ((EuclidGeom.Arc.cangle β).value.toReal < 0)

Instances For

source

def EuclidGeom.Arc.IsMinor {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} (β : EuclidGeom.Arc P ω) :

Prop

Equations

EuclidGeom.Arc.IsMinor β = ((EuclidGeom.Arc.cangle β).value.toReal > 0)

Instances For

source

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

EuclidGeom.Angle P

Equations

EuclidGeom.Chord.cangle s = ANG s.toSegND.source ω.center s.toSegND.target (_ : s.toSegND.source ≠ ω.center) (_ : s.toSegND.target ≠ ω.center)

Instances For

source

theorem EuclidGeom.Circle.cangle_of_arc_eq_cangle_of_toChord {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} (β : EuclidGeom.Arc P ω) :

EuclidGeom.Arc.cangle β = EuclidGeom.Chord.cangle (EuclidGeom.Arc.toChord β)

source

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

EuclidGeom.Chord.cangle s = EuclidGeom.Arc.cangle (EuclidGeom.Chord.toArc s)

source

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

(EuclidGeom.Chord.cangle s).value = ∠[Real.pi] ↔ EuclidGeom.Chord.IsDiameter s

source

theorem EuclidGeom.Arc.complement_cangle_reverse {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} (β : EuclidGeom.Arc P ω) :

EuclidGeom.Arc.cangle (EuclidGeom.Arc.complement β) = (EuclidGeom.Arc.cangle β).reverse

source

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

EuclidGeom.Chord.cangle (EuclidGeom.Chord.reverse s) = (EuclidGeom.Chord.cangle s).reverse

source

theorem EuclidGeom.Circle.cangle_of_complementary_arc_eq_neg {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} (β : EuclidGeom.Arc P ω) :

(EuclidGeom.Arc.cangle (EuclidGeom.Arc.complement β)).value = -(EuclidGeom.Arc.cangle β).value

source

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

(EuclidGeom.Chord.cangle (EuclidGeom.Chord.reverse s)).value = -(EuclidGeom.Chord.cangle s).value

source

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

(EuclidGeom.Chord.cangle s₁).value = (EuclidGeom.Chord.cangle s₂).value ↔ EuclidGeom.Chord.length s₁ = EuclidGeom.Chord.length s₂

source

def EuclidGeom.Arc.IsIangle {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} (β : EuclidGeom.Arc P ω) (ang : EuclidGeom.Angle P) :

Prop

Equations

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

Instances For

source

def EuclidGeom.Chord.IsIangle {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} (s : EuclidGeom.Chord P ω) (ang : EuclidGeom.Angle P) :

Prop

Equations

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

Instances For

source

theorem EuclidGeom.Arc.iangle_eq {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} {β : EuclidGeom.Arc P ω} {ang : EuclidGeom.Angle P} (h : EuclidGeom.Arc.IsIangle β ang) :

ANG β.source ang.source β.target (_ : β.source ≠ ang.source) (_ : β.target ≠ ang.source) = ang

source

theorem EuclidGeom.Chord.iangle_eq {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} {s : EuclidGeom.Chord P ω} {ang : EuclidGeom.Angle P} (h : EuclidGeom.Chord.IsIangle s ang) :

ANG s.toSegND.source ang.source s.toSegND.target (_ : s.toSegND.source ≠ ang.source) (_ : s.toSegND.target ≠ ang.source) = ang

source

theorem EuclidGeom.Arc.angle_mk_pt_is_iangle {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} {C : P} {β : EuclidGeom.Arc P ω} (h₁ : EuclidGeom.lies_on C ω) (h₂ : EuclidGeom.Arc.ne_endpts C β) :

EuclidGeom.Arc.IsIangle β (ANG β.source C β.target (_ : β.source ≠ C) (_ : β.target ≠ C))

source

theorem EuclidGeom.Chord.angle_mk_pt_is_iangle {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} {C : P} {s : EuclidGeom.Chord P ω} (h₁ : EuclidGeom.lies_on C ω) (h₂ : EuclidGeom.Chord.ne_endpts C s) :

EuclidGeom.Chord.IsIangle s (ANG s.toSegND.source C s.toSegND.target (_ : s.toSegND.source ≠ C) (_ : s.toSegND.target ≠ C))

source

theorem EuclidGeom.Circle.iangle_of_arc_is_iangle_of_toChord {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} {β : EuclidGeom.Arc P ω} {ang : EuclidGeom.Angle P} (h : EuclidGeom.Arc.IsIangle β ang) :

EuclidGeom.Chord.IsIangle (EuclidGeom.Arc.toChord β) ang

source

theorem EuclidGeom.Circle.iangle_of_chord_is_iangle_of_toArc {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} {s : EuclidGeom.Chord P ω} {ang : EuclidGeom.Angle P} (h : EuclidGeom.Chord.IsIangle s ang) :

EuclidGeom.Arc.IsIangle (EuclidGeom.Chord.toArc s) ang

source

theorem EuclidGeom.Arc.cangle_eq_two_times_inscribed_angle {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} {β : EuclidGeom.Arc P ω} {ang : EuclidGeom.Angle P} (h : EuclidGeom.Arc.IsIangle β ang) :

(EuclidGeom.Arc.cangle β).value = 2 • ang.value

source

theorem EuclidGeom.Chord.cangle_eq_two_times_inscribed_angle {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} {s : EuclidGeom.Chord P ω} {ang : EuclidGeom.Angle P} (h : EuclidGeom.Chord.IsIangle s ang) :

(EuclidGeom.Chord.cangle s).value = 2 • ang.value

source

theorem EuclidGeom.Circle.iangle_of_diameter_eq_mod_pi {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} {s : EuclidGeom.Chord P ω} {ang : EuclidGeom.Angle P} (h : EuclidGeom.Chord.IsIangle s ang) (hd : EuclidGeom.Chord.IsDiameter s) :

ang.dvalue = ↑∠[Real.pi / 2]

source

theorem EuclidGeom.Arc.iangle_invariant_mod_pi {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} {β : EuclidGeom.Arc P ω} {ang₁ : EuclidGeom.Angle P} {ang₂ : EuclidGeom.Angle P} (h₁ : EuclidGeom.Arc.IsIangle β ang₁) (h₂ : EuclidGeom.Arc.IsIangle β ang₂) :

ang₁.dvalue = ang₂.dvalue

source

theorem EuclidGeom.Chord.iangle_invariant_mod_pi {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} {s : EuclidGeom.Chord P ω} {ang₁ : EuclidGeom.Angle P} {ang₂ : EuclidGeom.Angle P} (h₁ : EuclidGeom.Chord.IsIangle s ang₁) (h₂ : EuclidGeom.Chord.IsIangle s ang₂) :

ang₁.dvalue = ang₂.dvalue

source

theorem EuclidGeom.Circle.dvalue_eq_of_lies_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} {A : P} {B : P} {C : P} {D : P} [_hca : EuclidGeom.PtNe C A] [_hda : EuclidGeom.PtNe D A] [_hcb : EuclidGeom.PtNe C B] [_hdb : EuclidGeom.PtNe D B] (ha : EuclidGeom.lies_on A ω) (hb : EuclidGeom.lies_on B ω) (hc : EuclidGeom.lies_on C ω) (hd : EuclidGeom.lies_on D ω) :

∡ A C B = ∡ A D B

source

def EuclidGeom.Arc.iangdv {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} (β : EuclidGeom.Arc P ω) :

EuclidGeom.AngDValue

Equations

EuclidGeom.Arc.iangdv β = ↑(EuclidGeom.AngValue.half (EuclidGeom.Arc.cangle β).value)

Instances For

source

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

EuclidGeom.AngDValue

Equations

EuclidGeom.Chord.iangdv s = ↑(EuclidGeom.AngValue.half (EuclidGeom.Chord.cangle s).value)

Instances For

source

theorem EuclidGeom.Arc.iangle_dvalue_eq {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} {β : EuclidGeom.Arc P ω} {ang : EuclidGeom.Angle P} (h : EuclidGeom.Arc.IsIangle β ang) :

ang.dvalue = EuclidGeom.Arc.iangdv β

source

theorem EuclidGeom.Chord.iangle_dvalue_eq {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} {s : EuclidGeom.Chord P ω} {ang : EuclidGeom.Angle P} (h : EuclidGeom.Chord.IsIangle s ang) :

ang.dvalue = EuclidGeom.Chord.iangdv s

source

theorem EuclidGeom.Circle.same_chord_same_iangle_dvalue {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} {s₁ : EuclidGeom.Chord P ω} {s₂ : EuclidGeom.Chord P ω} {ang₁ : EuclidGeom.Angle P} {ang₂ : EuclidGeom.Angle P} (h₁ : EuclidGeom.Chord.IsIangle s₁ ang₁) (h₂ : EuclidGeom.Chord.IsIangle s₂ ang₂) (h : EuclidGeom.Chord.length s₁ = EuclidGeom.Chord.length s₂) :

ang₁.dvalue = ang₂.dvalue