Documentation

EuclideanGeometry.Foundation.Construction.Triangle.PerpendicularBisector

source
structure EuclidGeom.IsPerpBis {P : Type u_1} [EuclidGeom.EuclideanPlane P] (seg_nd : EuclidGeom.SegND P) (line : EuclidGeom.Line P) :
Prop
    Instances For
      source
      def EuclidGeom.SegND.PerpBis {P : Type u_1} [EuclidGeom.EuclideanPlane P] (seg_nd : EuclidGeom.SegND P) :
      EuclidGeom.Line P
      Equations
      Instances For
        source
        theorem EuclidGeom.SegND.perp_bis_is_perp_bis {P : Type u_1} [EuclidGeom.EuclideanPlane P] (seg_nd : EuclidGeom.SegND P) :
        EuclidGeom.IsPerpBis seg_nd (EuclidGeom.SegND.PerpBis seg_nd)
        source
        structure EuclidGeom.IsCircumcenter {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) (O : P) :
        Prop
          Instances For
            source
            def EuclidGeom.TriangleND.Circumcenter {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) :
            P
            Equations
            Instances For
              source
              theorem EuclidGeom.TriangleND.circumcenter_is_circumcenter {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) :
              EuclidGeom.IsCircumcenter tr_nd (EuclidGeom.TriangleND.Circumcenter tr_nd)
              source
              structure EuclidGeom.IsCircumcircle {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) (cir : EuclidGeom.Circle P) :
              Prop
                Instances For
                  source
                  def EuclidGeom.TriangleND.Circumcircle {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) :
                  EuclidGeom.Circle P
                  Equations
                  Instances For
                    source
                    theorem EuclidGeom.TriangleND.circumcircle_is_circumcircle {P : Type u_1} [EuclidGeom.EuclideanPlane P] (tr_nd : EuclidGeom.TriangleND P) :
                    EuclidGeom.IsCircumcircle tr_nd (EuclidGeom.TriangleND.Circumcircle tr_nd)