AffineSubspace.direction_le
∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
[S : AddTorsor V P] {s₁ s₂ : AffineSubspace k P}, s₁ ≤ s₂ → s₁.direction ≤ s₂.directionIf one affine subspace is less than or equal to another, the same applies to their directions.
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 27 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Modulestatement and proof · cited by 20,661
- AddCommGroupstatement and proof · cited by 12,871
- Ringstatement and proof · cited by 7,463
- Submodulestatement · cited by 7,192
- AddTorsorstatement and proof · cited by 1,657
- AffineSubspacestatement and proof · cited by 871
- AffineSubspace.directionstatement · cited by 339
- vectorSpan_monoproof · cited by 7
Cited by13
Results whose statement or proof uses this declaration.
- AffineSubspace.inclusionproof · cited by 39
- EuclideanGeometry.Sphere.orthRadius_le_orthRadius_iffproof · cited by 2
- AffineSubspace.direction_lt_of_nonemptyproof · cited by 1
- Affine.Triangle.altitude_replace_orthocenter_eq_affineSpanproof · cited by 1
- AffineMap.restrict.linear_auxproof · cited by 1
- EuclideanGeometry.affineSpan_of_orthocentricSystemproof · cited by 1
- EuclideanGeometry.orthogonalProjection_orthogonalProjection_of_leproof · cited by 1
- EuclideanGeometry.Sphere.IsTangentAt.eq_orthRadius_of_finrank_add_one_eqproof · cited by 1
- AffineSubspace.inclusion_linearstatement · cited by 0
- AffineIndependent.card_le_card_of_subset_affineSpanproof · cited by 0