Affine and Euclidean geometry

ClassAffine space#

An AddTorsor G P gives a structure to the nonempty type P, acted on by an AddGroup G with a transitive and free action given by the +ᵥ operation and a corresponding subtraction given by the -ᵥ operation. In the case of a vector space, it is an affine space.

AddTorsor.{u_1, u_2} (G : outParam (Type u_1)) (P : Type u_2) [AddGroup G] : Type (max u_1 u_2)
Sources
MathlibAddTorsor
Uses 1 · Used by 14
Statement usesInteger
Used byFundamental Theorem of Integral Calculus · Principle of isolated zeros · Carathéodory's theorem · Fundamental theorem of calculus, part 2 · Finite-dimensional normed spaces over complete normed fields are complete · Corners theorem · Roth's theorem · Affine function · Affine subspace · Euclidean affine space · Radon's theorem · Affine groups · Differentiability of integrals with respect to parameters · Cauchy formulas

StructureAffine function#

An AffineMap k P1 P2 (notation: P1 →ᵃ[k] P2) is a map from P1 to P2 that induces a corresponding linear map from V1 to V2.

AffineMap.{u_1, u_2, u_3, u_4, u_5} (k : Type u_1) {V1 : Type u_2} (P1 : Type u_3) {V2 : Type u_4}
  (P2 : Type u_5) [Ring k] [AddCommGroup V1] [_root_.Module k V1] [AddTorsor V1 P1]
  [AddCommGroup V2] [_root_.Module k V2] [AddTorsor V2 P2] : Type (max (max (max u_2 u_3) u_4) u_5)
Sources
MathlibAffineMap
Uses 2 · Used by 13
Statement usesAffine space · Linear map
Used byProduct of Segments of Chords · Theorem of Ceva · Maximum modulus principle · Schwarz lemma · Barycenter · Urysohn's lemma · Apollonius's theorem · British flag theorem · Exterior angle theorem · Geometric mean theorem · Intersecting secants theorem · Tangent-secant theorem · Thales's theorem

StructureAffine subspace#

An AffineSubspace k P is a subset of an AffineSpace V P that, if not empty, has an affine space structure induced by a corresponding subspace of the Module k V.

AffineSubspace.{u_1, u_2, u_3} (k : Type u_1) {V : Type u_2} (P : Type u_3) [Ring k]
  [AddCommGroup V] [_root_.Module k V] [AddTorsor V P] : Type u_3
Sources
MathlibAffineSubspace
Uses 3 · Used by 1
Statement usesAffine space · Module · Ring
Used byAffine span

DefinitionBarycenter#

A weighted sum of the results of subtracting a default base point from the given points, added to that base point, as an affine map on the weights. This is intended to be used when the sum of the weights is 1, in which case it is an affine combination (barycenter) of the points with the given weights; that condition is specified as a hypothesis on those lemmas that require it.

Finset.affineCombination.{u_1, u_2, u_3, u_4} (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k]
  [AddCommGroup V] [_root_.Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι)
  (p : ι → P) : (ι → k) →ᵃ[k] P
Sources
MathlibFinset.affineCombination
Uses 2 · Used by 1
Statement usesAffine function · Finite set
Used byCommandino's theorem

DefinitionAffine span#

The affine span of a set of points is the smallest affine subspace containing those points. (Actually defined here in terms of spans in modules.)

affineSpan.{u_1, u_2, u_3} (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V]
  [_root_.Module k V] [AddTorsor V P] (s : Set P) : AffineSubspace k P
Sources
MathlibaffineSpan
Uses 2 · Used by 5
Statement usesAffine subspace · Generating sets
Used byProduct of Segments of Chords · Theorem of Ceva · Intersecting secants theorem · Tangent-secant theorem · Continuity (continuity and differentiability of convex functions)

ClassEuclidean affine space#

A NormedAddTorsor V P is a torsor of an additive seminormed group action by a SeminormedAddCommGroup V on points P. We bundle the pseudometric space structure and require the distance to be the same as results from the norm (which in fact implies the distance yields a pseudometric space, but bundling just the distance and using an instance for the pseudometric space results in type class problems).

NormedAddTorsor.{u_1, u_2} (V : outParam (Type u_1)) (P : Type u_2) [SeminormedAddCommGroup V]
  [PseudoMetricSpace P] : Type (max u_1 u_2)
Sources
MathlibNormedAddTorsor
Uses 3 · Used by 28
Statement usesAffine space · Bornology · Order
Used byPythagorean Theorem · Sum of the Angles of a Triangle · Heron’s Formula · Product of Segments of Chords · Isosceles Triangle Theorem · Theorem of Ceva · Ptolemy’s Theorem · The Law of Cosines · Maximum modulus principle · Removable singularity · Change of variables formula · Banach open mapping theorem · Urysohn's lemma · Apollonius's theorem · British flag theorem · CPCTC · Exterior angle theorem · Geometric mean theorem · Intersecting secants theorem · Stewart's theorem · Tangent-secant theorem · Thales's theorem · Dirichlet's approximation theorem · Cocyclicity · Isometries of a Euclidean affine space · Grönwall lemma · Continuity (continuity and differentiability of convex functions) · Differentiability of the limit of a sequence of functions

DefinitionAngle#

The undirected angle between two vectors. If either vector is 0, this is π/2. See Orientation.oangle for the corresponding oriented angle definition.

InnerProductGeometry.angle.{u_1} {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V]
  (x y : V) : ℝ
Sources
MathlibInnerProductGeometry.angle
Uses 2 · Used by 15
Statement usesInner product space, over \(R\) or \(C\) · Inverse trigonometric functions
Used byPythagorean Theorem · Sum of the Angles of a Triangle · Heron’s Formula · Product of Segments of Chords · Isosceles Triangle Theorem · Ptolemy’s Theorem · The Law of Cosines · British flag theorem · CPCTC · Exterior angle theorem · Geometric mean theorem · Intersecting secants theorem · Stewart's theorem · Tangent-secant theorem · Thales's theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.