structure EuclidGeom.IsAngBis {P : Type u_1} [EuclidGeom.EuclideanPlane P] (ang : EuclidGeom.Angle P) (ray : EuclidGeom.Ray P) : Prop

• eq_source : ang.source = ray.source
• eq_value : (EuclidGeom.Angle.mk_dir₁ ang ray.toDir).value = (EuclidGeom.Angle.mk_dir₂ ang ray.toDir).value
• same_sgn : (EuclidGeom.Angle.mk_dir₁ ang ray.toDir).value.IsPos ∧ ang.value.IsPos ∨ (EuclidGeom.Angle.mk_dir₁ ang ray.toDir).value.IsNeg ∧ ang.value.IsNeg ∨ (EuclidGeom.Angle.mk_dir₁ ang ray.toDir).value = ∠[Real.pi / 2] ∧ ang.value = ∠[Real.pi] ∨ (EuclidGeom.Angle.mk_dir₁ ang ray.toDir).value = 0 ∧ ang.value = 0

structure EuclidGeom.IsAngBisLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] (ang : EuclidGeom.Angle P) (l : EuclidGeom.Line P) : Prop

• source_on : EuclidGeom.lies_on ang.source l

structure EuclidGeom.IsExAngBis : Type

structure EuclidGeom.IsExAngBiscetorLine : Type

def EuclidGeom.Angle.AngBis {P : Type u_1} [EuclidGeom.EuclideanPlane P] (ang : EuclidGeom.Angle P) : EuclidGeom.Ray P

Equations

• EuclidGeom.Angle.AngBis ang = { source := ang.source, toDir := EuclidGeom.AngValue.half ang.value +ᵥ ang.dir₁ }

def EuclidGeom.Angle.AngBisLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] (ang : EuclidGeom.Angle P) : EuclidGeom.Line P

Equations

• EuclidGeom.Angle.AngBisLine ang = (EuclidGeom.Angle.AngBis ang).toLine

def EuclidGeom.Angle.ExAngBis {P : Type u_1} [EuclidGeom.EuclideanPlane P] (ang : EuclidGeom.Angle P) : EuclidGeom.Ray P

Equations

• EuclidGeom.Angle.ExAngBis ang = { source := ang.source, toDir := ∠[ang.value.toReal / 2 + Real.pi / 2] +ᵥ ang.dir₁ }

def EuclidGeom.Angle.ExAngBisLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] (ang : EuclidGeom.Angle P) : EuclidGeom.Line P

Equations

• EuclidGeom.Angle.ExAngBisLine ang = (EuclidGeom.Angle.ExAngBis ang).toLine

theorem EuclidGeom.Angle.eq_source {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} : ang.source = (EuclidGeom.Angle.AngBis ang).source

theorem EuclidGeom.Angle.value_angBis_eq_half_value {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} : (EuclidGeom.Angle.mk_dir₁ ang (EuclidGeom.Angle.AngBis ang).toDir).value = EuclidGeom.AngValue.half ang.value

theorem EuclidGeom.Angle.mk_start_ray_value_eq_half_angvalue {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} : (EuclidGeom.Angle.mk_dir₁ ang (EuclidGeom.Angle.AngBis ang).toDir).value.toReal = ang.value.toReal / 2

theorem EuclidGeom.Angle.angbis_is_angbis {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} : EuclidGeom.IsAngBis ang (EuclidGeom.Angle.AngBis ang)

theorem EuclidGeom.Angle.angbis_iff_angbis {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} {r : EuclidGeom.Ray P} : EuclidGeom.IsAngBis ang r ↔ r = EuclidGeom.Angle.AngBis ang

theorem EuclidGeom.Angle.ang_source_rev_eq_source_bis {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} {r : EuclidGeom.Ray P} (h : EuclidGeom.IsAngBis ang r) : ang.reverse.source = r.source

theorem EuclidGeom.Angle.nonpi_bisector_eq_bisector_of_rev {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} {r : EuclidGeom.Ray P} (h : EuclidGeom.IsAngBis ang r) (nonpi : ang.value ≠ ∠[Real.pi]) : EuclidGeom.IsAngBis ang.reverse r

theorem EuclidGeom.Angle.bisector_eq_bisector_of_rev' {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ang : EuclidGeom.Angle P} : EuclidGeom.Angle.AngBis ang = EuclidGeom.Angle.AngBis ang.reverse

theorem EuclidGeom.Angle.angbisline_is_angbisline : sorryAx (Sort u_2)

theorem EuclidGeom.Angle.exangbis_is_exangbis : sorryAx (Sort u_2)

theorem EuclidGeom.Angle.exangbisline_is_exangbisline : sorryAx (Sort u_2)

theorem EuclidGeom.lie_on_angbis {P : Type u_1} [EuclidGeom.EuclideanPlane P] (ang : EuclidGeom.Angle P) (A : P) [h : EuclidGeom.PtNe A ang.source] : EuclidGeom.lies_on A (EuclidGeom.Angle.AngBis ang) ↔ EuclidGeom.IsAngBis ang (RAY ang.source A)

theorem EuclidGeom.lie_on_angbisline_of_distance_zero {P : Type u_1} [EuclidGeom.EuclideanPlane P] (ang : EuclidGeom.Angle P) : sorryAx (Sort u_2)

theorem EuclidGeom.lie_on_angbis_of_lie_on_angbisline_inside_angle {P : Type u_1} [EuclidGeom.EuclideanPlane P] (ang : EuclidGeom.Angle P) : sorryAx (Sort u_2)

structure EuclidGeom.IsIncenter {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tri_nd : EuclidGeom.TriangleND P) (I : P) : Prop

structure EuclidGeom.IsExcenter1 {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tri_nd : EuclidGeom.TriangleND P) (E : P) : Prop

structure EuclidGeom.IsIncircle {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tri_nd : EuclidGeom.TriangleND P) (cir : EuclidGeom.Circle P) : Prop

structure EuclidGeom.IsExcircle1 {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tri_nd : EuclidGeom.TriangleND P) (cir : EuclidGeom.Circle P) : Prop

theorem EuclidGeom.TriangleND.angbisline_of_angle₁_angle₂_not_parallel {P : Type u_1} [EuclidGeom.EuclideanPlane P] {tri_nd : EuclidGeom.TriangleND P} : ¬EuclidGeom.Parallel (EuclidGeom.Angle.AngBis tri_nd.angle₁).toLine (EuclidGeom.Angle.AngBis tri_nd.angle₂).toLine

def EuclidGeom.TriangleND.Incenter {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tri_nd : EuclidGeom.TriangleND P) : P

Equations

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

def EuclidGeom.TriangleND.Excenter1 {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tri_nd : EuclidGeom.TriangleND P) : P

Equations

• EuclidGeom.TriangleND.Excenter1 tri_nd = sorryAx P

def EuclidGeom.TriangleND.Incircle {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tri_nd : EuclidGeom.TriangleND P) : EuclidGeom.Circle P

Equations

• EuclidGeom.TriangleND.Incircle tri_nd = sorryAx (EuclidGeom.Circle P)

def EuclidGeom.TriangleND.Excircle1 {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tri_nd : EuclidGeom.TriangleND P) : EuclidGeom.Circle P

Equations

• EuclidGeom.TriangleND.Excircle1 tri_nd = sorryAx (EuclidGeom.Circle P)

theorem EuclidGeom.TriangleND.incenter_is_incenter : sorryAx (Sort u_2)

theorem EuclidGeom.TriangleND.excenter1_is_excenter1 : sorryAx (Sort u_2)

theorem EuclidGeom.TriangleND.incircle_is_incircle : sorryAx (Sort u_2)

theorem EuclidGeom.TriangleND.excircle1_is_excircle1 : sorryAx (Sort u_2)

theorem EuclidGeom.incenter_lies_int_triangle {P : Type u_1} [EuclidGeom.EuclideanPlane P] (TriangleND : EuclidGeom.TriangleND P) : sorryAx (Sort u_2)