Theorems · Theorem · convex and discrete geometry
right_mem_segment
∀ (𝕜 : Type u_1) {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
[ZeroLEOneClass 𝕜] [inst_4 : MulActionWithZero 𝕜 E] (x y : E), y ∈ segment 𝕜 x y- Defined in
- Mathlib.Analysis.Convex.Segment
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 15 from the axioms · uses propext, Quot.sound
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.
- Setstatement · cited by 53,352
- Semiringstatement and proof · cited by 13,802
- AddCommMonoidstatement and proof · cited by 12,281
- PartialOrderstatement and proof · cited by 6,410
- ZeroLEOneClassstatement and proof · cited by 304
- segmentstatement · cited by 120
- MulActionWithZerostatement and proof · cited by 79
- segment_symmproof · cited by 9
- left_mem_segmentproof · cited by 8
Cited by7
Results whose statement or proof uses this declaration.
- convexHull_pairproof · cited by 3
- Convex.closure_interior_eq_closure_of_nonempty_interiorproof · cited by 3
- Convex.isLittleO_pow_succproof · cited by 1
- not_disjoint_segment_convexHull_tripleproof · cited by 1
- Sion.exists_lt_iInf_of_lt_iInf_of_supproof · cited by 1
- MeasureTheory.laverage_union_mem_segmentproof · cited by 0
- MeasureTheory.average_union_mem_segmentproof · cited by 0