Theorems · Theorem · geometry

AffineSubspace.direction_sup

∀ {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₂ : AffineSubspace k P} {p₁ p₂ : P},
  p₁ ∈ s₁ → p₂ ∈ s₂ → (s₁ ⊔ s₂).direction = s₁.direction ⊔ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁)

The direction of the sup of two nonempty affine subspaces is the sup of the two directions and of any one difference between points in the two subspaces.

Defined in

Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Cited by

2 results in Mathlib

Foundations

Depth 66 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingAddCommGroupModuleAddTorsor