affineSpan_mono
∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[inst_3 : AddTorsor V P] {s₁ s₂ : Set P}, s₁ ⊆ s₂ → affineSpan k s₁ ≤ affineSpan k s₂affineSpan is monotone.
- Cited by
- 21 results in Mathlib
- Foundations
- Depth 31 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- 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
- AddTorsorstatement and proof · cited by 1,657
- AffineSubspacestatement · cited by 871
- affineSpanstatement · cited by 417
- Set.Subset.transproof · cited by 218
- subset_affineSpanproof · cited by 18
- affineSpan_le_of_subset_coeproof · cited by 6
Cited by21
Results whose statement or proof uses this declaration.
- Affine.Simplex.touchpoint_mem_affineSpan_simplexproof · cited by 4
- Affine.Simplex.affineSpan_face_leproof · cited by 2
- Affine.Simplex.affineSpan_range_medialproof · cited by 2
- Affine.Simplex.closedInterior_face_subset_closedInteriorproof · cited by 2
- Affine.Simplex.altitudeFoot_mem_affineSpanproof · cited by 2
- affineSpan_convexHullproof · cited by 2
- Affine.Simplex.abs_inner_vsub_altitudeFoot_lt_mulproof · cited by 2
- collinear_insert_insert_of_mem_affineSpan_pairproof · cited by 1
- IsClosed.convexHull_subset_affineSpan_isVisibleproof · cited by 1
- EuclideanGeometry.affineSpan_of_orthocentricSystemproof · cited by 1
- IsOpen.affineSpan_eq_topproof · cited by 1