Euclidean affine spaces

StructureIsometries of a Euclidean affine space#

An affine isometric equivalence between two normed vector spaces, denoted f : P ≃ᵃⁱ[𝕜] P₂.

AffineIsometryEquiv.{u_1, u_2, u_4, u_7, u_8} (𝕜 : Type u_1) {V : Type u_2} {V₂ : Type u_4}
  (P : Type u_7) (P₂ : Type u_8) [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V]
  [PseudoMetricSpace P] [NormedAddTorsor V P] [SeminormedAddCommGroup V₂] [NormedSpace 𝕜 V₂]
  [PseudoMetricSpace P₂] [NormedAddTorsor V₂ P₂] : Type (max (max (max u_2 u_4) u_7) u_8)
Sources
MathlibAffineIsometryEquiv
Uses 3 · Used by 1
Statement usesEuclidean affine space · Linear map · Normed vector space over a normed field
Used byGroup of isometries of a Euclidean affine space

InstanceGroup of isometries of a Euclidean affine space#

The group of affine isometries of a NormedAddTorsor, P.

AffineIsometryEquiv.instGroup.{u_1, u_2, u_7} {𝕜 : Type u_1} {V : Type u_2} {P : Type u_7}
  [NormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [PseudoMetricSpace P]
  [NormedAddTorsor V P] : Group (P ≃ᵃⁱ[𝕜] P)
Sources
MathlibAffineIsometryEquiv.instGroup
Uses 1
Statement usesIsometries of a Euclidean affine space

TheoremInscribed angle theorem#

Oriented vector angle version of "angles in same segment are equal" and "opposite angles of a cyclic quadrilateral add to π", for oriented angles mod π (for which those are the same result), represented here as equality of twice the angles.

Orientation.two_zsmul_oangle_sub_eq_two_zsmul_oangle_sub_of_norm_eq.{u_1} {V : Type u_1}
  [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x₁ x₂ y z : V} (hx₁yne : x₁ ≠ y) (hx₁zne : x₁ ≠ z)
  (hx₂yne : x₂ ≠ y) (hx₂zne : x₂ ≠ z) {r : ℝ} (hx₁ : ‖x₁‖ = r) (hx₂ : ‖x₂‖ = r) (hy : ‖y‖ = r)
  (hz : ‖z‖ = r) : 2 • o.oangle (y - x₁) (z - x₁) = 2 • o.oangle (y - x₂) (z - x₂)
Sources
MathlibOrientation.two_zsmul_oangle_sub_eq_two_zsmul_oangle_sub_of_norm_eq
Uses 10
Statement usesCardinal · Continuous linear map · Determinant of vectors · Existence of orthonormal basis · Finite-dimensionality · Inverse trigonometric functions · Isomorphism with \(K^n\) · Linear independence · Orientation of a \(\R\)-vector space · Range of a linear map

StructureCocyclicity#

A set of points is concyclic if it is cospherical and coplanar. (Most results are stated directly in terms of Cospherical instead of using Concyclic.)

EuclideanGeometry.Concyclic.{u_1, u_2} {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V]
  [NormedSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (ps : Set P) : Prop
Sources
MathlibEuclideanGeometry.Concyclic
Uses 5
Statement usesCardinal · Euclidean affine space · Generating sets · Linear independence · Normed vector space over a normed field

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.