Theorems · Theorem · convex and discrete geometry
openSegment_eq_image_lineMap
∀ (𝕜 : Type u_1) {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [AddRightMono 𝕜] [inst_3 : AddCommGroup E]
[inst_4 : Module 𝕜 E] (x y : E), openSegment 𝕜 x y = ⇑(AffineMap.lineMap x y) '' Set.Ioo 0 1- Defined in
- Mathlib.Analysis.Convex.Segment
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 46 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Setstatement and proof · cited by 53,352
- Modulestatement and proof · cited by 20,661
- AddCommGroupstatement and proof · cited by 12,871
- Ringstatement and proof · cited by 7,463
- PartialOrderstatement and proof · cited by 6,410
- Set.imagestatement and proof · cited by 5,609
- Set.Ioostatement and proof · cited by 1,214
- AffineMapstatement · cited by 674
- Set.image_congrproof · cited by 533
- AddRightMonostatement and proof · cited by 367
- AffineMap.lineMapstatement and proof · cited by 254
Cited by6
Results whose statement or proof uses this declaration.
- image_openSegmentproof · cited by 5
- midpoint_mem_openSegmentproof · cited by 3
- sub_mem_posTangentConeAt_of_openSegment_subsetproof · cited by 2
- Convex.closure_subset_image_homothety_interior_of_one_ltproof · cited by 2
- openSegment_subset_unionproof · cited by 1
- lineMap_mem_openSegmentproof · cited by 1