CircleGeometry.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.EuclideanRamsey.CircleConsequence.circle_parameter_eq_zero_or_one line 10

Source documentation

Three points on a real circle cannot occupy three distinct parameters on a secant. No positive-radius assumption is needed.

theorem circle_parameter_eq_zero_or_one
    (x₀ x₁ y₀ y₁ c₀ c₁ R t : ℝ)
    (hx : (x₀-c₀)^2 + (x₁-c₁)^2 = R)
    (hy : (y₀-c₀)^2 + (y₁-c₁)^2 = R)
    (hz : (x₀+t*(y₀-x₀)-c₀)^2 + (x₁+t*(y₁-x₁)-c₁)^2 = R)
    (hxy : x₀ ≠ y₀ ∨ x₁ ≠ y₁) : t = 0 ∨ t = 1 := by
…

theorem OAI.EuclideanRamsey.CircleConsequence.secant_nonzero line 29

Source documentation

The determinant of a secant line is nonzero at a third distinct point on the same circle. Distinctness excludes radius zero.

theorem secant_nonzero
    (x₀ x₁ y₀ y₁ z₀ z₁ c₀ c₁ R : ℝ)
    (hx : (x₀-c₀)^2 + (x₁-c₁)^2 = R)
    (hy : (y₀-c₀)^2 + (y₁-c₁)^2 = R)
    (hz : (z₀-c₀)^2 + (z₁-c₁)^2 = R)
    (hxy : x₀ ≠ y₀ ∨ x₁ ≠ y₁)
    (hxz : x₀ ≠ z₀ ∨ x₁ ≠ z₁)
    (hyz : y₀ ≠ z₀ ∨ y₁ ≠ z₁) :
    (y₀-x₀)*(z₁-x₁) - (y₁-x₁)*(z₀-x₀) ≠ 0 := by
…

theorem OAI.EuclideanRamsey.CircleConsequence.ramsey_restrict line 75
Source documentation
Restriction of a Ramsey configuration preserves its distances.
```
theorem ramsey_restrict {s t d : ℕ} (a : Fin t → Space d)
    (f : Fin s → Fin t) (ha : Ramsey a) : Ramsey (a ∘ f) := by
…
```
Mentions: OAI.EuclideanRamsey.Space, OAI.EuclideanRamsey.Ramsey
theorem OAI.EuclideanRamsey.CircleConsequence.zero_radius_ramsey line 85
Source documentation
A circle of zero radius is a singleton; repeated labels are allowed.
```
theorem zero_radius_ramsey {s : ℕ} (a : Fin s → Space 2)
    (c : Space 2) (h : ∀ i, dist (a i) c = 0) : Ramsey a := by
…
```
Mentions: OAI.EuclideanRamsey.Space, OAI.EuclideanRamsey.Ramsey
theorem OAI.EuclideanRamsey.CircleConsequence.circle_coordinates line 97
Source documentation
The metric circle equation implies the scalar coordinate equation.
```
theorem circle_coordinates {s : ℕ} (a : Fin s → Space 2)
    (c : Space 2) (r : ℝ) (hc : ∀ i, dist (a i) c = r) :
    ∀ i, (a i 0-c 0)^2 + (a i 1-c 1)^2 = r^2 := by
…
```
Mentions: OAI.EuclideanRamsey.Space