Theorems · Theorem · convex and discrete geometry

Convexity.IsAffineMap.const

∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} [inst : PartialOrder R] [inst_1 : Semiring R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : Convexity.ConvexSpace R M] [inst_4 : Convexity.ConvexSpace R N] (x : N),
  Convexity.IsAffineMap R fun x_1 => x

Defined in: Mathlib.Geometry.Convex.ConvexSpace.Defs
Cited by: 0 results in Mathlib
Foundations: Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: PartialOrder Semiring IsStrictOrderedRing Convexity.ConvexSpace Convexity.ConvexSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites9

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Semiringstatement and proof · cited by 13,802
PartialOrderstatement and proof · cited by 6,410
IsStrictOrderedRingstatement and proof · cited by 2,490
Convexity.ConvexSpacestatement and proof · cited by 176
Convexity.StdSimplexproof · cited by 123
Convexity.ConvexSpace.sConvexCombproof · cited by 59
Convexity.IsAffineMapstatement · cited by 33
Convexity.ConvexSpace.sConvexComb_singleproof · cited by 9
Convexity.StdSimplex.map_constproof · cited by 4

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.