ContinuousAffineMap.coe_lineMap_eq
∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
[inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] (p₀ p₁ : P) [inst_5 : TopologicalSpace R]
[inst_6 : TopologicalSpace V] [inst_7 : ContinuousSMul R V] [inst_8 : ContinuousVAdd V P],
⇑(ContinuousAffineMap.lineMap p₀ p₁) = ⇑(AffineMap.lineMap p₀ p₁)- Cited by
- 1 results in Mathlib
- Foundations
- Depth 76 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- TopologicalSpacestatement and proof · cited by 24,529
- Modulestatement and proof · cited by 20,661
- AddCommGroupstatement and proof · cited by 12,871
- Ringstatement and proof · cited by 7,463
- AddTorsorstatement and proof · cited by 1,657
- ContinuousSMulstatement and proof · cited by 1,016
- AffineMapstatement · cited by 674
- ContinuousAffineMapstatement · cited by 263
- AffineMap.lineMapstatement · cited by 254
- ContinuousVAddstatement and proof · cited by 52
- ContinuousAffineMap.lineMapstatement · cited by 8
Cited by1
Results whose statement or proof uses this declaration.
- Manifold.riemannianEDist_le_pathELengthproof · cited by 4