subset_affineSpan
∀ (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 : Set P), s ⊆ ↑(affineSpan k s)A set is contained in its affine span.
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 25 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 and proof · cited by 53,352
- Modulestatement and proof · cited by 20,661
- AddCommGroupstatement and proof · cited by 12,871
- SetLike.coestatement · cited by 8,199
- Ringstatement and proof · cited by 7,463
- AddTorsorstatement and proof · cited by 1,657
- AffineSubspacestatement · cited by 871
- affineSpanstatement · cited by 417
- subset_spanPointsproof · cited by 4
Cited by18
Results whose statement or proof uses this declaration.
- affineSpan_monoproof · cited by 21
- AffineSubspace.map_spanproof · cited by 16
- AffineSubspace.affineSpan_coeproof · cited by 4
- subset_intrinsicClosureproof · cited by 2
- convexHull_subset_affineSpanproof · cited by 2
- affineSpan_induction'statement and proof · cited by 2
- intrinsicClosure_eq_closureproof · cited by 2
- Affine.Simplex.orthogonalProjection_eq_circumcenter_of_exists_dist_eqproof · cited by 2
- IsClosed.convexHull_subset_affineSpan_isVisibleproof · cited by 1
- Real.Convex.dimH_eq_finrank_vectorSpanproof · cited by 1
- AffineSubspace.span_univproof · cited by 1
- IsClosed.intrinsicClosureproof · cited by 1