Documentation

EuclideanGeometry.Foundation.Axiom.Circle.Basic

theorem EuclidGeom.Circle.ext_iff {P : Type u_1} :

∀ {inst : EuclidGeom.EuclideanPlane P} (x y : EuclidGeom.Circle P), x = y ↔ x.center = y.center ∧ x.radius = y.radius

theorem EuclidGeom.Circle.ext {P : Type u_1} :

∀ {inst : EuclidGeom.EuclideanPlane P} (x y : EuclidGeom.Circle P), x.center = y.center → x.radius = y.radius → x = y

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

Type u_1

center : P
radius : ℝ
rad_pos : 0 < s.radius

Instances For

def EuclidGeom.Circle.mk_pt_pt {P : Type u_1} [EuclidGeom.EuclideanPlane P] (O : P) (A : P) [h : EuclidGeom.PtNe O A] :

EuclidGeom.Circle P

Equations

EuclidGeom.Circle.mk_pt_pt O A = { center := O, radius := dist O A, rad_pos := (_ : 0 < dist O A) }

Instances For

def EuclidGeom.Circle.mk_pt_pt_pt {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) (h : ¬EuclidGeom.Collinear A B C) :

EuclidGeom.Circle P

Equations

EuclidGeom.Circle.mk_pt_pt_pt A B C h = sorryAx (EuclidGeom.Circle P)

Instances For

def EuclidGeom.termCIR :

Lean.ParserDescr

Equations

EuclidGeom.termCIR = Lean.ParserDescr.node `EuclidGeom.termCIR 1024 (Lean.ParserDescr.symbol "CIR")

Instances For

def EuclidGeom.«term⨀» :

Lean.ParserDescr

Equations

EuclidGeom.«term⨀» = Lean.ParserDescr.node `EuclidGeom.term⨀ 1024 (Lean.ParserDescr.symbol "⨀")

Instances For

def EuclidGeom.Circle.mk_pt_radius {P : Type u_1} [EuclidGeom.EuclideanPlane P] (O : P) {r : ℝ} (rpos : r > 0) :

EuclidGeom.Circle P

Equations

EuclidGeom.Circle.mk_pt_radius O rpos = { center := O, radius := r, rad_pos := rpos }

Instances For

def EuclidGeom.Circle.mk_pt_pt_diam {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) [_h : EuclidGeom.PtNe A B] :

EuclidGeom.Circle P

Equations

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

Instances For

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

Equations

EuclidGeom.Circle.IsInside p ω = (dist ω.center p ≤ ω.radius)

Instances For

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

Equations

EuclidGeom.Circle.IsOn p ω = (dist ω.center p = ω.radius)

Instances For

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

Equations

EuclidGeom.Circle.IsInt p ω = (dist ω.center p < ω.radius)

Instances For

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

Equations

EuclidGeom.Circle.IsOutside p ω = (ω.radius < dist ω.center p)

Instances For

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

Equations

EuclidGeom.Circle.carrier ω = {p : P | EuclidGeom.Circle.IsOn p ω}

Instances For

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

Equations

EuclidGeom.Circle.interior ω = {p : P | EuclidGeom.Circle.IsInt p ω}

Instances For

instance EuclidGeom.Circle.instFigCircle {P : Type u_1} [EuclidGeom.EuclideanPlane P] :

EuclidGeom.Fig (EuclidGeom.Circle P) P

Equations

EuclidGeom.Circle.instFigCircle = { carrier := EuclidGeom.Circle.carrier }

instance EuclidGeom.Circle.instInteriorCircle {P : Type u_1} [EuclidGeom.EuclideanPlane P] :

EuclidGeom.Interior (EuclidGeom.Circle P) P

Equations

EuclidGeom.Circle.instInteriorCircle = { interior := EuclidGeom.Circle.interior }

def EuclidGeom.term_LiesIn_ :

Lean.TrailingParserDescr

Equations

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

Instances For

def EuclidGeom.term_LiesOut_ :

Lean.TrailingParserDescr

Equations

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

Instances For

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

EuclidGeom.PtNe p ω.center

Equations

(_ : EuclidGeom.PtNe p ω.center) = (_ : Fact (p ≠ ω.center))

instance EuclidGeom.Circle.pt_lieson_ne_center {P : Type u_1} [EuclidGeom.EuclideanPlane P] {p : P} {ω : EuclidGeom.Circle P} (h : EuclidGeom.lies_on p ω) :

EuclidGeom.PtNe p ω.center

Equations

(_ : EuclidGeom.PtNe p ω.center) = (_ : Fact (p ≠ ω.center))

instance EuclidGeom.Circle.pt_liesout_ne_pt_lieson {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {ω : EuclidGeom.Circle P} (h₁ : EuclidGeom.Circle.IsOutside A ω) (h₂ : EuclidGeom.lies_on B ω) :

EuclidGeom.PtNe A B

Equations

(_ : EuclidGeom.PtNe A B) = (_ : Fact (A ≠ B))

instance EuclidGeom.Circle.pt_liesint_ne_pt_lieson {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {ω : EuclidGeom.Circle P} (h₁ : EuclidGeom.lies_int A ω) (h₂ : EuclidGeom.lies_on B ω) :

EuclidGeom.PtNe A B

Equations

(_ : EuclidGeom.PtNe A B) = (_ : Fact (A ≠ B))

instance EuclidGeom.Circle.pt_liesout_ne_pt_liesint {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {ω : EuclidGeom.Circle P} (h₁ : EuclidGeom.Circle.IsOutside A ω) (h₂ : EuclidGeom.lies_int B ω) :

EuclidGeom.PtNe A B

Equations

(_ : EuclidGeom.PtNe A B) = (_ : Fact (A ≠ B))

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

EuclidGeom.lies_int p ω ↔ EuclidGeom.Circle.IsInside p ω ∧ ¬EuclidGeom.lies_on p ω

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

EuclidGeom.Circle.IsInside A ω ↔ EuclidGeom.lies_int A ω ∨ EuclidGeom.lies_on A ω

theorem EuclidGeom.Circle.mk_pt_pt_lieson {P : Type u_1} [EuclidGeom.EuclideanPlane P] {O : P} {A : P} [EuclidGeom.PtNe O A] :

EuclidGeom.lies_on A (EuclidGeom.Circle.mk_pt_pt O A)

theorem EuclidGeom.Circle.mk_pt_pt_diam_fst_lieson {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} [_h : EuclidGeom.PtNe A B] :

EuclidGeom.lies_on A (EuclidGeom.Circle.mk_pt_pt_diam A B)

theorem EuclidGeom.Circle.mk_pt_pt_diam_snd_lieson {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} [_h : EuclidGeom.PtNe A B] :

EuclidGeom.lies_on B (EuclidGeom.Circle.mk_pt_pt_diam A B)

def EuclidGeom.Circle.seg_lies_inside_circle {P : Type u_1} [EuclidGeom.EuclideanPlane P] (l : EuclidGeom.Seg P) (ω : EuclidGeom.Circle P) :

Equations

EuclidGeom.Circle.seg_lies_inside_circle l ω = (EuclidGeom.Circle.IsInside l.source ω ∧ EuclidGeom.Circle.IsInside l.target ω)

Instances For

def EuclidGeom.term_SegInCir_ :

Lean.TrailingParserDescr

Equations

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

Instances For

theorem EuclidGeom.Circle.pt_lies_inside_circle_of_seg_inside_circle {P : Type u_1} [EuclidGeom.EuclideanPlane P] {l : EuclidGeom.Seg P} {ω : EuclidGeom.Circle P} (h : EuclidGeom.Circle.seg_lies_inside_circle l ω) {p : P} (lieson : EuclidGeom.lies_int p l) :

EuclidGeom.lies_int p ω

theorem EuclidGeom.Circle.pts_lieson_circle_vec_eq {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {ω : EuclidGeom.Circle P} [hne : EuclidGeom.PtNe B A] (hl₁ : EuclidGeom.lies_on A ω) (hl₂ : EuclidGeom.lies_on B ω) :

EuclidGeom.Vec.mkPtPt A (EuclidGeom.perp_foot ω.center (LIN A B)) = EuclidGeom.Vec.mkPtPt (EuclidGeom.perp_foot ω.center (LIN A B)) B

theorem EuclidGeom.Circle.pts_lieson_circle_perpfoot_eq_midpoint {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {ω : EuclidGeom.Circle P} [hne : EuclidGeom.PtNe B A] (hl₁ : EuclidGeom.lies_on A ω) (hl₂ : EuclidGeom.lies_on B ω) :

EuclidGeom.perp_foot ω.center (LIN A B) = { source := A, target := B }.midpoint

theorem EuclidGeom.Circle.three_pts_lieson_circle_not_collinear {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} {ω : EuclidGeom.Circle P} [hne₁ : EuclidGeom.PtNe B A] [hne₂ : EuclidGeom.PtNe C B] [hne₃ : EuclidGeom.PtNe A C] (hl₁ : EuclidGeom.lies_on A ω) (hl₂ : EuclidGeom.lies_on B ω) (hl₃ : EuclidGeom.lies_on C ω) :

¬EuclidGeom.Collinear A B C

def EuclidGeom.Circle.IsAntipode {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} (ω : EuclidGeom.Circle P) (_ha : EuclidGeom.lies_on A ω) (_hb : EuclidGeom.lies_on B ω) :

Equations

EuclidGeom.Circle.IsAntipode ω _ha _hb = (B = EuclidGeom.pt_flip A ω.center)

Instances For

theorem EuclidGeom.Circle.antipode_symm {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {ω : EuclidGeom.Circle P} (ha : EuclidGeom.lies_on A ω) (hb : EuclidGeom.lies_on B ω) :

EuclidGeom.Circle.IsAntipode ω ha hb ↔ EuclidGeom.Circle.IsAntipode ω hb ha

theorem EuclidGeom.Circle.antipode_center_is_midpoint {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {ω : EuclidGeom.Circle P} (ha : EuclidGeom.lies_on A ω) (hb : EuclidGeom.lies_on B ω) (h : EuclidGeom.Circle.IsAntipode ω ha hb) :

ω.center = { source := A, target := B }.midpoint

theorem EuclidGeom.Circle.antipode_iff_collinear {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) {ω : EuclidGeom.Circle P} [h : EuclidGeom.PtNe B A] (ha : EuclidGeom.lies_on A ω) (hb : EuclidGeom.lies_on B ω) :

EuclidGeom.Circle.IsAntipode ω ha hb ↔ EuclidGeom.Collinear A ω.center B

theorem EuclidGeom.Circle.mk_pt_pt_diam_isantipode {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} [h : EuclidGeom.PtNe A B] :

EuclidGeom.Circle.IsAntipode (EuclidGeom.Circle.mk_pt_pt_diam A B) (_ : EuclidGeom.lies_on A (EuclidGeom.Circle.mk_pt_pt_diam A B)) (_ : EuclidGeom.lies_on B (EuclidGeom.Circle.mk_pt_pt_diam A B))

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

∀ {inst : EuclidGeom.EuclideanPlane P} {ω : EuclidGeom.Circle P} (x y : EuclidGeom.Arc P ω), x = y ↔ x.source = y.source ∧ x.target = y.target

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

∀ {inst : EuclidGeom.EuclideanPlane P} {ω : EuclidGeom.Circle P} (x y : EuclidGeom.Arc P ω), x.source = y.source → x.target = y.target → x = y

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

Type u_2

source : P
target : P
ison : EuclidGeom.lies_on s.source ω ∧ EuclidGeom.lies_on s.target ω
endpts_ne : EuclidGeom.PtNe s.target s.source

Instances For

def EuclidGeom.Arc.mk_pt_pt_circle {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} {A : P} {B : P} [h : EuclidGeom.PtNe B A] (ha : EuclidGeom.lies_on A ω) (hb : EuclidGeom.lies_on B ω) :

EuclidGeom.Arc P ω

Equations

EuclidGeom.Arc.mk_pt_pt_circle ha hb = { source := A, target := B, ison := (_ : EuclidGeom.lies_on A ω ∧ EuclidGeom.lies_on B ω), endpts_ne := h }

Instances For

def EuclidGeom.termARC :

Lean.ParserDescr

Equations

EuclidGeom.termARC = Lean.ParserDescr.node `EuclidGeom.termARC 1024 (Lean.ParserDescr.symbol "ARC")

Instances For

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

Equations

EuclidGeom.Arc.IsOn p β = (EuclidGeom.lies_on p ω ∧ ¬EuclidGeom.IsOnLeftSide p (DLIN β.source β.target (_ : β.target ≠ β.source)))

Instances For

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

Equations

EuclidGeom.Arc.ne_endpts p β = (p ≠ β.source ∧ p ≠ β.target)

Instances For

instance EuclidGeom.Arc.pt_ne_source {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} {p : P} {β : EuclidGeom.Arc P ω} (h : EuclidGeom.Arc.ne_endpts p β) :

EuclidGeom.PtNe β.source p

Equations

(_ : EuclidGeom.PtNe β.source p) = (_ : Fact (β.source ≠ p))

instance EuclidGeom.Arc.pt_ne_target {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} {p : P} {β : EuclidGeom.Arc P ω} (h : EuclidGeom.Arc.ne_endpts p β) :

EuclidGeom.PtNe β.target p

Equations

(_ : EuclidGeom.PtNe β.target p) = (_ : Fact (β.target ≠ p))

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

Equations

EuclidGeom.Arc.IsInt p β = (EuclidGeom.Arc.IsOn p β ∧ EuclidGeom.Arc.ne_endpts p β)

Instances For

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

Equations

EuclidGeom.Arc.carrier β = {p : P | EuclidGeom.Arc.IsOn p β}

Instances For

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

Equations

EuclidGeom.Arc.interior β = {p : P | EuclidGeom.Arc.IsInt p β}

Instances For

instance EuclidGeom.Arc.instFigArc {P : Type u_1} [EuclidGeom.EuclideanPlane P] (ω : EuclidGeom.Circle P) :

EuclidGeom.Fig (EuclidGeom.Arc P ω) P

Equations

EuclidGeom.Arc.instFigArc ω = { carrier := EuclidGeom.Arc.carrier }

instance EuclidGeom.Arc.instInteriorArc {P : Type u_1} [EuclidGeom.EuclideanPlane P] (ω : EuclidGeom.Circle P) :

EuclidGeom.Interior (EuclidGeom.Arc P ω) P

Equations

EuclidGeom.Arc.instInteriorArc ω = { interior := EuclidGeom.Arc.interior }

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

EuclidGeom.Arc.ne_endpts ω.center β

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

EuclidGeom.PtNe β.source ω.center

Equations

(_ : EuclidGeom.PtNe β.source ω.center) = (_ : Fact (β.source ≠ ω.center))

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

EuclidGeom.PtNe β.target ω.center

Equations

(_ : EuclidGeom.PtNe β.target ω.center) = (_ : Fact (β.target ≠ ω.center))

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

EuclidGeom.Arc P ω

Equations

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

Instances For

theorem EuclidGeom.Arc.pt_liesint_not_lieson_dlin {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} {β : EuclidGeom.Arc P ω} {p : P} (h : EuclidGeom.lies_int p β) :

¬EuclidGeom.lies_on p (DLIN β.source β.target)

theorem EuclidGeom.Arc.pt_liesint_liesonright_dlin {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} {β : EuclidGeom.Arc P ω} {p : P} (h : EuclidGeom.lies_int p β) :

EuclidGeom.IsOnRightSide p (DLIN β.source β.target)

theorem EuclidGeom.Arc.pt_liesint_complementary_liesonleft_dlin {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} {β : EuclidGeom.Arc P ω} {p : P} (h : EuclidGeom.lies_int p (EuclidGeom.Arc.complement β)) :

EuclidGeom.IsOnLeftSide p (DLIN β.source β.target)

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

∀ {inst : EuclidGeom.EuclideanPlane P} {ω : EuclidGeom.Circle P} (x y : EuclidGeom.Chord P ω), x.toSegND = y.toSegND → x = y

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

∀ {inst : EuclidGeom.EuclideanPlane P} {ω : EuclidGeom.Circle P} (x y : EuclidGeom.Chord P ω), x = y ↔ x.toSegND = y.toSegND

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

Type u_2

toSegND : EuclidGeom.SegND P
ison : EuclidGeom.lies_on s.toSegND.source ω ∧ EuclidGeom.lies_on s.toSegND.target ω

Instances For

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

EuclidGeom.PtNe s.toSegND.source s.toSegND.target

Equations

(_ : EuclidGeom.PtNe s.toSegND.source s.toSegND.target) = (_ : Fact (s.toSegND.source ≠ s.toSegND.target))

def EuclidGeom.Chord.mk_pt_pt_circle {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} {A : P} {B : P} [h : EuclidGeom.PtNe A B] (ha : EuclidGeom.lies_on A ω) (hb : EuclidGeom.lies_on B ω) :

EuclidGeom.Chord P ω

Equations

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

Instances For

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

Equations

EuclidGeom.Chord.IsOn A s = EuclidGeom.lies_on A s.toSegND

Instances For

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

Equations

EuclidGeom.Chord.IsInt A s = EuclidGeom.lies_int A s.toSegND

Instances For

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

Equations

EuclidGeom.Chord.carrier s = {p : P | EuclidGeom.Chord.IsOn p s}

Instances For

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

Equations

EuclidGeom.Chord.interior s = {p : P | EuclidGeom.Chord.IsInt p s}

Instances For

instance EuclidGeom.Chord.instFigChord {P : Type u_1} [EuclidGeom.EuclideanPlane P] (ω : EuclidGeom.Circle P) :

EuclidGeom.Fig (EuclidGeom.Chord P ω) P

Equations

EuclidGeom.Chord.instFigChord ω = { carrier := EuclidGeom.Chord.carrier }

instance EuclidGeom.Chord.instInteriorChord {P : Type u_1} [EuclidGeom.EuclideanPlane P] (ω : EuclidGeom.Circle P) :

EuclidGeom.Interior (EuclidGeom.Chord P ω) P

Equations

EuclidGeom.Chord.instInteriorChord ω = { interior := EuclidGeom.Chord.interior }

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

Equations

EuclidGeom.Chord.ne_endpts A s = (A ≠ s.toSegND.source ∧ A ≠ s.toSegND.target)

Instances For

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

EuclidGeom.Chord.ne_endpts ω.center s

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

EuclidGeom.PtNe s.toSegND.source ω.center

Equations

(_ : EuclidGeom.PtNe s.toSegND.source ω.center) = (_ : Fact (s.toSegND.source ≠ ω.center))

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

EuclidGeom.PtNe s.toSegND.target ω.center

Equations

(_ : EuclidGeom.PtNe s.toSegND.target ω.center) = (_ : Fact (s.toSegND.target ≠ ω.center))

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

EuclidGeom.Chord P ω

Equations

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

Instances For

theorem EuclidGeom.Chord.pt_liesint_liesint_circle {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ω : EuclidGeom.Circle P} {A : P} {s : EuclidGeom.Chord P ω} (h : EuclidGeom.lies_int A s) :

EuclidGeom.lies_int A ω

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

EuclidGeom.Chord P ω

Equations

EuclidGeom.Arc.toChord β = { toSegND := SEG_nd β.source β.target (_ : β.target ≠ β.source), ison := (_ : EuclidGeom.lies_on β.source ω ∧ EuclidGeom.lies_on β.target ω) }

Instances For

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

EuclidGeom.Arc P ω

Equations

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

Instances For

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

EuclidGeom.Arc.toChord (EuclidGeom.Arc.complement β) = EuclidGeom.Chord.reverse (EuclidGeom.Arc.toChord β)

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

EuclidGeom.Chord.toArc (EuclidGeom.Chord.reverse s) = EuclidGeom.Arc.complement (EuclidGeom.Chord.toArc s)

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

Equations

EuclidGeom.Chord.length s = EuclidGeom.SegND.length s.toSegND

Instances For

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

Equations

EuclidGeom.Chord.IsDiameter s = EuclidGeom.lies_on ω.center s

Instances For

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

EuclidGeom.Chord.IsDiameter s ↔ EuclidGeom.Circle.IsAntipode ω (_ : EuclidGeom.lies_on s.toSegND.source ω) (_ : EuclidGeom.lies_on s.toSegND.target ω)

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

EuclidGeom.Chord.length s = 2 * ω.radius