Documentation

Mathlib.LinearAlgebra.AffineSpace.AffineSubspace

Affine spaces #

This file defines affine subspaces (over modules) and the affine span of a set of points.

Main definitions #

Implementation notes #

outParam is used in the definition of AddTorsor V P to make V an implicit argument (deduced from P) in most cases. As for modules, k is an explicit argument rather than implied by P or V.

This file only provides purely algebraic definitions and results. Those depending on analysis or topology are defined elsewhere; see Analysis.NormedSpace.AddTorsor and Topology.Algebra.Affine.

References #

def vectorSpan (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : Set P) :

The submodule spanning the differences of a (possibly empty) set of points.

Equations
Instances For
    theorem vectorSpan_def (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : Set P) :

    The definition of vectorSpan, for rewriting.

    theorem vectorSpan_mono (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s₁ : Set P} {s₂ : Set P} (h : s₁ s₂) :
    vectorSpan k s₁ vectorSpan k s₂

    vectorSpan is monotone.

    @[simp]
    theorem vectorSpan_empty (k : Type u_1) {V : Type u_2} (P : Type u_3) [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] :

    The vectorSpan of the empty set is .

    @[simp]
    theorem vectorSpan_singleton (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (p : P) :

    The vectorSpan of a single point is .

    theorem vsub_set_subset_vectorSpan (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : Set P) :
    s -ᵥ s (vectorSpan k s)

    The s -ᵥ s lies within the vectorSpan k s.

    theorem vsub_mem_vectorSpan (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : Set P} {p1 : P} {p2 : P} (hp1 : p1 s) (hp2 : p2 s) :
    p1 -ᵥ p2 vectorSpan k s

    Each pairwise difference is in the vectorSpan.

    def spanPoints (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : Set P) :
    Set P

    The points in the affine span of a (possibly empty) set of points. Use affineSpan instead to get an AffineSubspace k P.

    Equations
    Instances For
      theorem mem_spanPoints (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (p : P) (s : Set P) :
      p sp spanPoints k s

      A point in a set is in its affine span.

      theorem subset_spanPoints (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : Set P) :

      A set is contained in its spanPoints.

      @[simp]
      theorem spanPoints_nonempty (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : Set P) :
      (spanPoints k s).Nonempty s.Nonempty

      The spanPoints of a set is nonempty if and only if that set is.

      theorem vadd_mem_spanPoints_of_mem_spanPoints_of_mem_vectorSpan (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : Set P} {p : P} {v : V} (hp : p spanPoints k s) (hv : v vectorSpan k s) :

      Adding a point in the affine span and a vector in the spanning submodule produces a point in the affine span.

      theorem vsub_mem_vectorSpan_of_mem_spanPoints_of_mem_spanPoints (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : Set P} {p1 : P} {p2 : P} (hp1 : p1 spanPoints k s) (hp2 : p2 spanPoints k s) :
      p1 -ᵥ p2 vectorSpan k s

      Subtracting two points in the affine span produces a vector in the spanning submodule.

      structure AffineSubspace (k : Type u_1) {V : Type u_2} (P : Type u_3) [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] :
      Type u_3

      An AffineSubspace k P is a subset of an AffineSpace V P that, if not empty, has an affine space structure induced by a corresponding subspace of the Module k V.

      • carrier : Set P

        The affine subspace seen as a subset.

      • smul_vsub_vadd_mem : ∀ (c : k) {p1 p2 p3 : P}, p1 self.carrierp2 self.carrierp3 self.carrierc (p1 -ᵥ p2) +ᵥ p3 self.carrier
      Instances For
        theorem AffineSubspace.smul_vsub_vadd_mem {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (self : AffineSubspace k P) (c : k) {p1 : P} {p2 : P} {p3 : P} :
        p1 self.carrierp2 self.carrierp3 self.carrierc (p1 -ᵥ p2) +ᵥ p3 self.carrier
        def Submodule.toAffineSubspace {k : Type u_1} {V : Type u_2} [Ring k] [AddCommGroup V] [Module k V] (p : Submodule k V) :

        Reinterpret p : Submodule k V as an AffineSubspace k V.

        Equations
        • p.toAffineSubspace = { carrier := p, smul_vsub_vadd_mem := }
        Instances For
          instance AffineSubspace.instSetLike (k : Type u_1) {V : Type u_2} (P : Type u_3) [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] :
          Equations
          theorem AffineSubspace.mem_coe (k : Type u_1) {V : Type u_2} (P : Type u_3) [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (p : P) (s : AffineSubspace k P) :
          p s p s

          A point is in an affine subspace coerced to a set if and only if it is in that affine subspace.

          def AffineSubspace.direction {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : AffineSubspace k P) :

          The direction of an affine subspace is the submodule spanned by the pairwise differences of points. (Except in the case of an empty affine subspace, where the direction is the zero submodule, every vector in the direction is the difference of two points in the affine subspace.)

          Equations
          Instances For
            theorem AffineSubspace.direction_eq_vectorSpan {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : AffineSubspace k P) :
            s.direction = vectorSpan k s

            The direction equals the vectorSpan.

            def AffineSubspace.directionOfNonempty {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : AffineSubspace k P} (h : (s).Nonempty) :

            Alternative definition of the direction when the affine subspace is nonempty. This is defined so that the order on submodules (as used in the definition of Submodule.span) can be used in the proof of coe_direction_eq_vsub_set, and is not intended to be used beyond that proof.

            Equations
            Instances For
              theorem AffineSubspace.directionOfNonempty_eq_direction {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : AffineSubspace k P} (h : (s).Nonempty) :

              direction_of_nonempty gives the same submodule as direction.

              theorem AffineSubspace.coe_direction_eq_vsub_set {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : AffineSubspace k P} (h : (s).Nonempty) :
              s.direction = s -ᵥ s

              The set of vectors in the direction of a nonempty affine subspace is given by vsub_set.

              theorem AffineSubspace.mem_direction_iff_eq_vsub {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : AffineSubspace k P} (h : (s).Nonempty) (v : V) :
              v s.direction p1s, p2s, v = p1 -ᵥ p2

              A vector is in the direction of a nonempty affine subspace if and only if it is the subtraction of two vectors in the subspace.

              theorem AffineSubspace.vadd_mem_of_mem_direction {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : AffineSubspace k P} {v : V} (hv : v s.direction) {p : P} (hp : p s) :
              v +ᵥ p s

              Adding a vector in the direction to a point in the subspace produces a point in the subspace.

              theorem AffineSubspace.vsub_mem_direction {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : AffineSubspace k P} {p1 : P} {p2 : P} (hp1 : p1 s) (hp2 : p2 s) :
              p1 -ᵥ p2 s.direction

              Subtracting two points in the subspace produces a vector in the direction.

              theorem AffineSubspace.vadd_mem_iff_mem_direction {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : AffineSubspace k P} (v : V) {p : P} (hp : p s) :
              v +ᵥ p s v s.direction

              Adding a vector to a point in a subspace produces a point in the subspace if and only if the vector is in the direction.

              theorem AffineSubspace.vadd_mem_iff_mem_of_mem_direction {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : AffineSubspace k P} {v : V} (hv : v s.direction) {p : P} :
              v +ᵥ p s p s

              Adding a vector in the direction to a point produces a point in the subspace if and only if the original point is in the subspace.

              theorem AffineSubspace.coe_direction_eq_vsub_set_right {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : AffineSubspace k P} {p : P} (hp : p s) :
              s.direction = (fun (x : P) => x -ᵥ p) '' s

              Given a point in an affine subspace, the set of vectors in its direction equals the set of vectors subtracting that point on the right.

              theorem AffineSubspace.coe_direction_eq_vsub_set_left {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : AffineSubspace k P} {p : P} (hp : p s) :
              s.direction = (fun (x : P) => p -ᵥ x) '' s

              Given a point in an affine subspace, the set of vectors in its direction equals the set of vectors subtracting that point on the left.

              theorem AffineSubspace.mem_direction_iff_eq_vsub_right {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : AffineSubspace k P} {p : P} (hp : p s) (v : V) :
              v s.direction p2s, v = p2 -ᵥ p

              Given a point in an affine subspace, a vector is in its direction if and only if it results from subtracting that point on the right.

              theorem AffineSubspace.mem_direction_iff_eq_vsub_left {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : AffineSubspace k P} {p : P} (hp : p s) (v : V) :
              v s.direction p2s, v = p -ᵥ p2

              Given a point in an affine subspace, a vector is in its direction if and only if it results from subtracting that point on the left.

              theorem AffineSubspace.vsub_right_mem_direction_iff_mem {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : AffineSubspace k P} {p : P} (hp : p s) (p2 : P) :
              p2 -ᵥ p s.direction p2 s

              Given a point in an affine subspace, a result of subtracting that point on the right is in the direction if and only if the other point is in the subspace.

              theorem AffineSubspace.vsub_left_mem_direction_iff_mem {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : AffineSubspace k P} {p : P} (hp : p s) (p2 : P) :
              p -ᵥ p2 s.direction p2 s

              Given a point in an affine subspace, a result of subtracting that point on the left is in the direction if and only if the other point is in the subspace.

              theorem AffineSubspace.coe_injective {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] :
              Function.Injective SetLike.coe

              Two affine subspaces are equal if they have the same points.

              theorem AffineSubspace.ext {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {p : AffineSubspace k P} {q : AffineSubspace k P} (h : ∀ (x : P), x p x q) :
              p = q
              theorem AffineSubspace.ext_iff {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s₁ : AffineSubspace k P) (s₂ : AffineSubspace k P) :
              s₁ = s₂ s₁ = s₂
              theorem AffineSubspace.ext_of_direction_eq {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s1 : AffineSubspace k P} {s2 : AffineSubspace k P} (hd : s1.direction = s2.direction) (hn : (s1 s2).Nonempty) :
              s1 = s2

              Two affine subspaces with the same direction and nonempty intersection are equal.

              @[reducible, inline]
              abbrev AffineSubspace.toAddTorsor {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : AffineSubspace k P) [Nonempty s] :
              AddTorsor s.direction s

              This is not an instance because it loops with AddTorsor.nonempty.

              Equations
              Instances For
                @[simp]
                theorem AffineSubspace.coe_vsub {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : AffineSubspace k P) [Nonempty s] (a : s) (b : s) :
                (a -ᵥ b) = a -ᵥ b
                @[simp]
                theorem AffineSubspace.coe_vadd {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : AffineSubspace k P) [Nonempty s] (a : s.direction) (b : s) :
                (a +ᵥ b) = a +ᵥ b
                def AffineSubspace.subtype {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : AffineSubspace k P) [Nonempty s] :
                s →ᵃ[k] P

                Embedding of an affine subspace to the ambient space, as an affine map.

                Equations
                • s.subtype = { toFun := Subtype.val, linear := s.direction.subtype, map_vadd' := }
                Instances For
                  @[simp]
                  theorem AffineSubspace.subtype_linear {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : AffineSubspace k P) [Nonempty s] :
                  s.subtype.linear = s.direction.subtype
                  theorem AffineSubspace.subtype_apply {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : AffineSubspace k P) [Nonempty s] (p : s) :
                  s.subtype p = p
                  @[simp]
                  theorem AffineSubspace.coeSubtype {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : AffineSubspace k P) [Nonempty s] :
                  s.subtype = Subtype.val
                  theorem AffineSubspace.injective_subtype {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : AffineSubspace k P) [Nonempty s] :
                  Function.Injective s.subtype
                  theorem AffineSubspace.eq_iff_direction_eq_of_mem {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s₁ : AffineSubspace k P} {s₂ : AffineSubspace k P} {p : P} (h₁ : p s₁) (h₂ : p s₂) :
                  s₁ = s₂ s₁.direction = s₂.direction

                  Two affine subspaces with nonempty intersection are equal if and only if their directions are equal.

                  def AffineSubspace.mk' {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (p : P) (direction : Submodule k V) :

                  Construct an affine subspace from a point and a direction.

                  Equations
                  Instances For
                    theorem AffineSubspace.self_mem_mk' {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (p : P) (direction : Submodule k V) :
                    p AffineSubspace.mk' p direction

                    An affine subspace constructed from a point and a direction contains that point.

                    theorem AffineSubspace.vadd_mem_mk' {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {v : V} (p : P) {direction : Submodule k V} (hv : v direction) :
                    v +ᵥ p AffineSubspace.mk' p direction

                    An affine subspace constructed from a point and a direction contains the result of adding a vector in that direction to that point.

                    theorem AffineSubspace.mk'_nonempty {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (p : P) (direction : Submodule k V) :
                    ((AffineSubspace.mk' p direction)).Nonempty

                    An affine subspace constructed from a point and a direction is nonempty.

                    @[simp]
                    theorem AffineSubspace.direction_mk' {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (p : P) (direction : Submodule k V) :
                    (AffineSubspace.mk' p direction).direction = direction

                    The direction of an affine subspace constructed from a point and a direction.

                    theorem AffineSubspace.mem_mk'_iff_vsub_mem {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {p₁ : P} {p₂ : P} {direction : Submodule k V} :
                    p₂ AffineSubspace.mk' p₁ direction p₂ -ᵥ p₁ direction

                    A point lies in an affine subspace constructed from another point and a direction if and only if their difference is in that direction.

                    @[simp]
                    theorem AffineSubspace.mk'_eq {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : AffineSubspace k P} {p : P} (hp : p s) :
                    AffineSubspace.mk' p s.direction = s

                    Constructing an affine subspace from a point in a subspace and that subspace's direction yields the original subspace.

                    theorem AffineSubspace.spanPoints_subset_coe_of_subset_coe {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : Set P} {s1 : AffineSubspace k P} (h : s s1) :
                    spanPoints k s s1

                    If an affine subspace contains a set of points, it contains the spanPoints of that set.

                    @[simp]
                    theorem Submodule.mem_toAffineSubspace {k : Type u_1} {V : Type u_2} [Ring k] [AddCommGroup V] [Module k V] {p : Submodule k V} {x : V} :
                    x p.toAffineSubspace x p
                    @[simp]
                    theorem Submodule.toAffineSubspace_direction {k : Type u_1} {V : Type u_2} [Ring k] [AddCommGroup V] [Module k V] (s : Submodule k V) :
                    s.toAffineSubspace.direction = s
                    theorem AffineMap.lineMap_mem {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {Q : AffineSubspace k P} {p₀ : P} {p₁ : P} (c : k) (h₀ : p₀ Q) (h₁ : p₁ Q) :
                    (AffineMap.lineMap p₀ p₁) c Q
                    def affineSpan (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : Set P) :

                    The affine span of a set of points is the smallest affine subspace containing those points. (Actually defined here in terms of spans in modules.)

                    Equations
                    Instances For
                      @[simp]
                      theorem coe_affineSpan (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : Set P) :
                      (affineSpan k s) = spanPoints k s

                      The affine span, converted to a set, is spanPoints.

                      theorem subset_affineSpan (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : Set P) :
                      s (affineSpan k s)

                      A set is contained in its affine span.

                      theorem direction_affineSpan (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : Set P) :
                      (affineSpan k s).direction = vectorSpan k s

                      The direction of the affine span is the vectorSpan.

                      theorem mem_affineSpan (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {p : P} {s : Set P} (hp : p s) :

                      A point in a set is in its affine span.

                      instance AffineSubspace.instCompleteLattice {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] :
                      Equations
                      instance AffineSubspace.instInhabited {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] :
                      Equations
                      • AffineSubspace.instInhabited = { default := }
                      theorem AffineSubspace.le_def {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] (s1 : AffineSubspace k P) (s2 : AffineSubspace k P) :
                      s1 s2 s1 s2

                      The order on subspaces is the same as that on the corresponding sets.

                      theorem AffineSubspace.le_def' {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] (s1 : AffineSubspace k P) (s2 : AffineSubspace k P) :
                      s1 s2 ps1, p s2

                      One subspace is less than or equal to another if and only if all its points are in the second subspace.

                      theorem AffineSubspace.lt_def {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] (s1 : AffineSubspace k P) (s2 : AffineSubspace k P) :
                      s1 < s2 s1 s2

                      The < order on subspaces is the same as that on the corresponding sets.

                      theorem AffineSubspace.not_le_iff_exists {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] (s1 : AffineSubspace k P) (s2 : AffineSubspace k P) :
                      ¬s1 s2 ps1, ps2

                      One subspace is not less than or equal to another if and only if it has a point not in the second subspace.

                      theorem AffineSubspace.exists_of_lt {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {s1 : AffineSubspace k P} {s2 : AffineSubspace k P} (h : s1 < s2) :
                      ps2, ps1

                      If a subspace is less than another, there is a point only in the second.

                      theorem AffineSubspace.lt_iff_le_and_exists {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] (s1 : AffineSubspace k P) (s2 : AffineSubspace k P) :
                      s1 < s2 s1 s2 ps2, ps1

                      A subspace is less than another if and only if it is less than or equal to the second subspace and there is a point only in the second.

                      theorem AffineSubspace.eq_of_direction_eq_of_nonempty_of_le {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {s₁ : AffineSubspace k P} {s₂ : AffineSubspace k P} (hd : s₁.direction = s₂.direction) (hn : (s₁).Nonempty) (hle : s₁ s₂) :
                      s₁ = s₂

                      If an affine subspace is nonempty and contained in another with the same direction, they are equal.

                      theorem AffineSubspace.affineSpan_eq_sInf (k : Type u_1) (V : Type u_2) {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] (s : Set P) :
                      affineSpan k s = sInf {s' : AffineSubspace k P | s s'}

                      The affine span is the sInf of subspaces containing the given points.

                      def AffineSubspace.gi (k : Type u_1) (V : Type u_2) (P : Type u_3) [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] :
                      GaloisInsertion (affineSpan k) SetLike.coe

                      The Galois insertion formed by affineSpan and coercion back to a set.

                      Equations
                      Instances For
                        @[simp]
                        theorem AffineSubspace.span_empty (k : Type u_1) (V : Type u_2) (P : Type u_3) [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] :

                        The span of the empty set is .

                        @[simp]
                        theorem AffineSubspace.span_univ (k : Type u_1) (V : Type u_2) (P : Type u_3) [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] :
                        affineSpan k Set.univ =

                        The span of univ is .

                        theorem affineSpan_le {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {s : Set P} {Q : AffineSubspace k P} :
                        affineSpan k s Q s Q
                        @[simp]
                        theorem AffineSubspace.coe_affineSpan_singleton (k : Type u_1) (V : Type u_2) {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] (p : P) :
                        (affineSpan k {p}) = {p}

                        The affine span of a single point, coerced to a set, contains just that point.

                        @[simp]
                        theorem AffineSubspace.mem_affineSpan_singleton (k : Type u_1) (V : Type u_2) {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {p₁ : P} {p₂ : P} :
                        p₁ affineSpan k {p₂} p₁ = p₂

                        A point is in the affine span of a single point if and only if they are equal.

                        @[simp]
                        theorem AffineSubspace.preimage_coe_affineSpan_singleton (k : Type u_1) (V : Type u_2) {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] (x : P) :
                        Subtype.val ⁻¹' {x} = Set.univ
                        theorem AffineSubspace.span_union (k : Type u_1) (V : Type u_2) {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] (s : Set P) (t : Set P) :

                        The span of a union of sets is the sup of their spans.

                        theorem AffineSubspace.span_iUnion (k : Type u_1) (V : Type u_2) {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} (s : ιSet P) :
                        affineSpan k (⋃ (i : ι), s i) = ⨆ (i : ι), affineSpan k (s i)

                        The span of a union of an indexed family of sets is the sup of their spans.

                        @[simp]
                        theorem AffineSubspace.top_coe (k : Type u_1) (V : Type u_2) (P : Type u_3) [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] :
                        = Set.univ

                        , coerced to a set, is the whole set of points.

                        @[simp]
                        theorem AffineSubspace.mem_top (k : Type u_1) (V : Type u_2) {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] (p : P) :

                        All points are in .

                        @[simp]
                        theorem AffineSubspace.direction_top (k : Type u_1) (V : Type u_2) (P : Type u_3) [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] :
                        .direction =

                        The direction of is the whole module as a submodule.

                        @[simp]
                        theorem AffineSubspace.bot_coe (k : Type u_1) (V : Type u_2) (P : Type u_3) [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] :
                        =

                        , coerced to a set, is the empty set.

                        theorem AffineSubspace.bot_ne_top (k : Type u_1) (V : Type u_2) (P : Type u_3) [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] :
                        instance AffineSubspace.instNontrivial (k : Type u_1) (V : Type u_2) (P : Type u_3) [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] :
                        Equations
                        • =
                        theorem AffineSubspace.nonempty_of_affineSpan_eq_top (k : Type u_1) (V : Type u_2) (P : Type u_3) [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {s : Set P} (h : affineSpan k s = ) :
                        s.Nonempty
                        theorem AffineSubspace.vectorSpan_eq_top_of_affineSpan_eq_top (k : Type u_1) (V : Type u_2) (P : Type u_3) [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {s : Set P} (h : affineSpan k s = ) :

                        If the affine span of a set is , then the vector span of the same set is the .

                        theorem AffineSubspace.affineSpan_eq_top_iff_vectorSpan_eq_top_of_nonempty (k : Type u_1) (V : Type u_2) (P : Type u_3) [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {s : Set P} (hs : s.Nonempty) :

                        For a nonempty set, the affine span is iff its vector span is .

                        For a non-trivial space, the affine span of a set is iff its vector span is .

                        theorem AffineSubspace.card_pos_of_affineSpan_eq_top (k : Type u_1) (V : Type u_2) (P : Type u_3) [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {ι : Type u_4} [Fintype ι] {p : ιP} (h : affineSpan k (Set.range p) = ) :
                        @[simp]
                        theorem AffineSubspace.topEquiv_apply (k : Type u_1) (V : Type u_2) (P : Type u_3) [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] (self : { x : P // x Set.univ }) :
                        (AffineSubspace.topEquiv k V P) self = self
                        @[simp]
                        theorem AffineSubspace.topEquiv_symm_apply_coe (k : Type u_1) (V : Type u_2) (P : Type u_3) [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] (a : P) :
                        ((AffineSubspace.topEquiv k V P).symm a) = a
                        @[simp]
                        theorem AffineSubspace.linear_topEquiv (k : Type u_1) (V : Type u_2) (P : Type u_3) [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] :
                        (AffineSubspace.topEquiv k V P).linear = (LinearEquiv.ofEq .direction ).trans Submodule.topEquiv
                        def AffineSubspace.topEquiv (k : Type u_1) (V : Type u_2) (P : Type u_3) [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] :

                        The top affine subspace is linearly equivalent to the affine space.

                        This is the affine version of Submodule.topEquiv.

                        Equations
                        Instances For
                          theorem AffineSubspace.not_mem_bot (k : Type u_1) (V : Type u_2) {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] (p : P) :
                          p

                          No points are in .

                          @[simp]
                          theorem AffineSubspace.direction_bot (k : Type u_1) (V : Type u_2) (P : Type u_3) [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] :
                          .direction =

                          The direction of is the submodule .

                          @[simp]
                          theorem AffineSubspace.coe_eq_bot_iff {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] (Q : AffineSubspace k P) :
                          Q = Q =
                          @[simp]
                          theorem AffineSubspace.coe_eq_univ_iff {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] (Q : AffineSubspace k P) :
                          Q = Set.univ Q =
                          theorem AffineSubspace.nonempty_iff_ne_bot {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] (Q : AffineSubspace k P) :
                          (Q).Nonempty Q
                          theorem AffineSubspace.eq_bot_or_nonempty {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] (Q : AffineSubspace k P) :
                          Q = (Q).Nonempty
                          theorem AffineSubspace.subsingleton_of_subsingleton_span_eq_top {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {s : Set P} (h₁ : s.Subsingleton) (h₂ : affineSpan k s = ) :
                          theorem AffineSubspace.eq_univ_of_subsingleton_span_eq_top {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {s : Set P} (h₁ : s.Subsingleton) (h₂ : affineSpan k s = ) :
                          s = Set.univ
                          @[simp]
                          theorem AffineSubspace.direction_eq_top_iff_of_nonempty {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {s : AffineSubspace k P} (h : (s).Nonempty) :
                          s.direction = s =

                          A nonempty affine subspace is if and only if its direction is .

                          @[simp]
                          theorem AffineSubspace.inf_coe {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] (s1 : AffineSubspace k P) (s2 : AffineSubspace k P) :
                          s1 s2 = s1 s2

                          The inf of two affine subspaces, coerced to a set, is the intersection of the two sets of points.

                          theorem AffineSubspace.mem_inf_iff {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] (p : P) (s1 : AffineSubspace k P) (s2 : AffineSubspace k P) :
                          p s1 s2 p s1 p s2

                          A point is in the inf of two affine subspaces if and only if it is in both of them.

                          theorem AffineSubspace.direction_inf {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] (s1 : AffineSubspace k P) (s2 : AffineSubspace k P) :
                          (s1 s2).direction s1.direction s2.direction

                          The direction of the inf of two affine subspaces is less than or equal to the inf of their directions.

                          theorem AffineSubspace.direction_inf_of_mem {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {s₁ : AffineSubspace k P} {s₂ : AffineSubspace k P} {p : P} (h₁ : p s₁) (h₂ : p s₂) :
                          (s₁ s₂).direction = s₁.direction s₂.direction

                          If two affine subspaces have a point in common, the direction of their inf equals the inf of their directions.

                          theorem AffineSubspace.direction_inf_of_mem_inf {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {s₁ : AffineSubspace k P} {s₂ : AffineSubspace k P} {p : P} (h : p s₁ s₂) :
                          (s₁ s₂).direction = s₁.direction s₂.direction

                          If two affine subspaces have a point in their inf, the direction of their inf equals the inf of their directions.

                          theorem AffineSubspace.direction_le {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {s1 : AffineSubspace k P} {s2 : AffineSubspace k P} (h : s1 s2) :
                          s1.direction s2.direction

                          If one affine subspace is less than or equal to another, the same applies to their directions.

                          theorem AffineSubspace.direction_lt_of_nonempty {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {s1 : AffineSubspace k P} {s2 : AffineSubspace k P} (h : s1 < s2) (hn : (s1).Nonempty) :
                          s1.direction < s2.direction

                          If one nonempty affine subspace is less than another, the same applies to their directions

                          theorem AffineSubspace.sup_direction_le {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] (s1 : AffineSubspace k P) (s2 : AffineSubspace k P) :
                          s1.direction s2.direction (s1 s2).direction

                          The sup of the directions of two affine subspaces is less than or equal to the direction of their sup.

                          theorem AffineSubspace.sup_direction_lt_of_nonempty_of_inter_empty {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {s1 : AffineSubspace k P} {s2 : AffineSubspace k P} (h1 : (s1).Nonempty) (h2 : (s2).Nonempty) (he : s1 s2 = ) :
                          s1.direction s2.direction < (s1 s2).direction

                          The sup of the directions of two nonempty affine subspaces with empty intersection is less than the direction of their sup.

                          theorem AffineSubspace.inter_nonempty_of_nonempty_of_sup_direction_eq_top {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {s1 : AffineSubspace k P} {s2 : AffineSubspace k P} (h1 : (s1).Nonempty) (h2 : (s2).Nonempty) (hd : s1.direction s2.direction = ) :
                          (s1 s2).Nonempty

                          If the directions of two nonempty affine subspaces span the whole module, they have nonempty intersection.

                          theorem AffineSubspace.inter_eq_singleton_of_nonempty_of_isCompl {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] {s1 : AffineSubspace k P} {s2 : AffineSubspace k P} (h1 : (s1).Nonempty) (h2 : (s2).Nonempty) (hd : IsCompl s1.direction s2.direction) :
                          ∃ (p : P), s1 s2 = {p}

                          If the directions of two nonempty affine subspaces are complements of each other, they intersect in exactly one point.

                          @[simp]
                          theorem AffineSubspace.affineSpan_coe {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] (s : AffineSubspace k P) :
                          affineSpan k s = s

                          Coercing a subspace to a set then taking the affine span produces the original subspace.

                          theorem vectorSpan_eq_span_vsub_set_left (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : Set P} {p : P} (hp : p s) :
                          vectorSpan k s = Submodule.span k ((fun (x : P) => p -ᵥ x) '' s)

                          The vectorSpan is the span of the pairwise subtractions with a given point on the left.

                          theorem vectorSpan_eq_span_vsub_set_right (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : Set P} {p : P} (hp : p s) :
                          vectorSpan k s = Submodule.span k ((fun (x : P) => x -ᵥ p) '' s)

                          The vectorSpan is the span of the pairwise subtractions with a given point on the right.

                          theorem vectorSpan_eq_span_vsub_set_left_ne (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : Set P} {p : P} (hp : p s) :
                          vectorSpan k s = Submodule.span k ((fun (x : P) => p -ᵥ x) '' (s \ {p}))

                          The vectorSpan is the span of the pairwise subtractions with a given point on the left, excluding the subtraction of that point from itself.

                          theorem vectorSpan_eq_span_vsub_set_right_ne (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : Set P} {p : P} (hp : p s) :
                          vectorSpan k s = Submodule.span k ((fun (x : P) => x -ᵥ p) '' (s \ {p}))

                          The vectorSpan is the span of the pairwise subtractions with a given point on the right, excluding the subtraction of that point from itself.

                          theorem vectorSpan_eq_span_vsub_finset_right_ne (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] [DecidableEq P] [DecidableEq V] {s : Finset P} {p : P} (hp : p s) :
                          vectorSpan k s = Submodule.span k (Finset.image (fun (x : P) => x -ᵥ p) (s.erase p))

                          The vectorSpan is the span of the pairwise subtractions with a given point on the right, excluding the subtraction of that point from itself.

                          theorem vectorSpan_image_eq_span_vsub_set_left_ne (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} (p : ιP) {s : Set ι} {i : ι} (hi : i s) :
                          vectorSpan k (p '' s) = Submodule.span k ((fun (x : P) => p i -ᵥ x) '' (p '' (s \ {i})))

                          The vectorSpan of the image of a function is the span of the pairwise subtractions with a given point on the left, excluding the subtraction of that point from itself.

                          theorem vectorSpan_image_eq_span_vsub_set_right_ne (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} (p : ιP) {s : Set ι} {i : ι} (hi : i s) :
                          vectorSpan k (p '' s) = Submodule.span k ((fun (x : P) => x -ᵥ p i) '' (p '' (s \ {i})))

                          The vectorSpan of the image of a function is the span of the pairwise subtractions with a given point on the right, excluding the subtraction of that point from itself.

                          theorem vectorSpan_range_eq_span_range_vsub_left (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} (p : ιP) (i0 : ι) :
                          vectorSpan k (Set.range p) = Submodule.span k (Set.range fun (i : ι) => p i0 -ᵥ p i)

                          The vectorSpan of an indexed family is the span of the pairwise subtractions with a given point on the left.

                          theorem vectorSpan_range_eq_span_range_vsub_right (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} (p : ιP) (i0 : ι) :
                          vectorSpan k (Set.range p) = Submodule.span k (Set.range fun (i : ι) => p i -ᵥ p i0)

                          The vectorSpan of an indexed family is the span of the pairwise subtractions with a given point on the right.

                          theorem vectorSpan_range_eq_span_range_vsub_left_ne (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} (p : ιP) (i₀ : ι) :
                          vectorSpan k (Set.range p) = Submodule.span k (Set.range fun (i : { x : ι // x i₀ }) => p i₀ -ᵥ p i)

                          The vectorSpan of an indexed family is the span of the pairwise subtractions with a given point on the left, excluding the subtraction of that point from itself.

                          theorem vectorSpan_range_eq_span_range_vsub_right_ne (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {ι : Type u_4} (p : ιP) (i₀ : ι) :
                          vectorSpan k (Set.range p) = Submodule.span k (Set.range fun (i : { x : ι // x i₀ }) => p i -ᵥ p i₀)

                          The vectorSpan of an indexed family is the span of the pairwise subtractions with a given point on the right, excluding the subtraction of that point from itself.

                          theorem affineSpan_nonempty (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : Set P} :
                          ((affineSpan k s)).Nonempty s.Nonempty

                          The affine span of a set is nonempty if and only if that set is.

                          theorem Set.Nonempty.affineSpan (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : Set P} :
                          s.Nonempty((affineSpan k s)).Nonempty

                          Alias of the reverse direction of affineSpan_nonempty.


                          The affine span of a set is nonempty if and only if that set is.

                          instance instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : Set P} [Nonempty s] :

                          The affine span of a nonempty set is nonempty.

                          Equations
                          • =
                          @[simp]
                          theorem affineSpan_eq_bot (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : Set P} :

                          The affine span of a set is if and only if that set is empty.

                          @[simp]
                          theorem bot_lt_affineSpan (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : Set P} :
                          < affineSpan k s s.Nonempty
                          theorem affineSpan_induction {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {x : P} {s : Set P} {p : PProp} (h : x affineSpan k s) (mem : xs, p x) (smul_vsub_vadd : ∀ (c : k) (u v w : P), p up vp wp (c (u -ᵥ v) +ᵥ w)) :
                          p x

                          An induction principle for span membership. If p holds for all elements of s and is preserved under certain affine combinations, then p holds for all elements of the span of s.

                          theorem affineSpan_induction' {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : Set P} {p : (x : P) → x affineSpan k sProp} (mem : ∀ (y : P) (hys : y s), p y ) (smul_vsub_vadd : ∀ (c : k) (u : P) (hu : u affineSpan k s) (v : P) (hv : v affineSpan k s) (w : P) (hw : w affineSpan k s), p u hup v hvp w hwp (c (u -ᵥ v) +ᵥ w) ) {x : P} (h : x affineSpan k s) :
                          p x h

                          A dependent version of affineSpan_induction.

                          @[simp]
                          theorem affineSpan_coe_preimage_eq_top {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (A : Set P) [Nonempty A] :
                          affineSpan k (Subtype.val ⁻¹' A) =

                          A set, considered as a subset of its spanned affine subspace, spans the whole subspace.

                          theorem affineSpan_singleton_union_vadd_eq_top_of_span_eq_top {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : Set V} (p : P) (h : Submodule.span k (Set.range Subtype.val) = ) :
                          affineSpan k ({p} (fun (v : V) => v +ᵥ p) '' s) =

                          Suppose a set of vectors spans V. Then a point p, together with those vectors added to p, spans P.

                          theorem vectorSpan_pair (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (p₁ : P) (p₂ : P) :
                          vectorSpan k {p₁, p₂} = Submodule.span k {p₁ -ᵥ p₂}

                          The vectorSpan of two points is the span of their difference.

                          theorem vectorSpan_pair_rev (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (p₁ : P) (p₂ : P) :
                          vectorSpan k {p₁, p₂} = Submodule.span k {p₂ -ᵥ p₁}

                          The vectorSpan of two points is the span of their difference (reversed).

                          theorem vsub_mem_vectorSpan_pair (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (p₁ : P) (p₂ : P) :
                          p₁ -ᵥ p₂ vectorSpan k {p₁, p₂}

                          The difference between two points lies in their vectorSpan.

                          theorem vsub_rev_mem_vectorSpan_pair (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (p₁ : P) (p₂ : P) :
                          p₂ -ᵥ p₁ vectorSpan k {p₁, p₂}

                          The difference between two points (reversed) lies in their vectorSpan.

                          theorem smul_vsub_mem_vectorSpan_pair {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (r : k) (p₁ : P) (p₂ : P) :
                          r (p₁ -ᵥ p₂) vectorSpan k {p₁, p₂}

                          A multiple of the difference between two points lies in their vectorSpan.

                          theorem smul_vsub_rev_mem_vectorSpan_pair {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (r : k) (p₁ : P) (p₂ : P) :
                          r (p₂ -ᵥ p₁) vectorSpan k {p₁, p₂}

                          A multiple of the difference between two points (reversed) lies in their vectorSpan.

                          theorem mem_vectorSpan_pair {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {p₁ : P} {p₂ : P} {v : V} :
                          v vectorSpan k {p₁, p₂} ∃ (r : k), r (p₁ -ᵥ p₂) = v

                          A vector lies in the vectorSpan of two points if and only if it is a multiple of their difference.

                          theorem mem_vectorSpan_pair_rev {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {p₁ : P} {p₂ : P} {v : V} :
                          v vectorSpan k {p₁, p₂} ∃ (r : k), r (p₂ -ᵥ p₁) = v

                          A vector lies in the vectorSpan of two points if and only if it is a multiple of their difference (reversed).

                          The line between two points, as an affine subspace.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            theorem left_mem_affineSpan_pair (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (p₁ : P) (p₂ : P) :
                            p₁ affineSpan k {p₁, p₂}

                            The first of two points lies in their affine span.

                            theorem right_mem_affineSpan_pair (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (p₁ : P) (p₂ : P) :
                            p₂ affineSpan k {p₁, p₂}

                            The second of two points lies in their affine span.

                            theorem AffineMap.lineMap_mem_affineSpan_pair {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (r : k) (p₁ : P) (p₂ : P) :
                            (AffineMap.lineMap p₁ p₂) r affineSpan k {p₁, p₂}

                            A combination of two points expressed with lineMap lies in their affine span.

                            theorem AffineMap.lineMap_rev_mem_affineSpan_pair {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (r : k) (p₁ : P) (p₂ : P) :
                            (AffineMap.lineMap p₂ p₁) r affineSpan k {p₁, p₂}

                            A combination of two points expressed with lineMap (with the two points reversed) lies in their affine span.

                            theorem smul_vsub_vadd_mem_affineSpan_pair {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (r : k) (p₁ : P) (p₂ : P) :
                            r (p₂ -ᵥ p₁) +ᵥ p₁ affineSpan k {p₁, p₂}

                            A multiple of the difference of two points added to the first point lies in their affine span.

                            theorem smul_vsub_rev_vadd_mem_affineSpan_pair {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (r : k) (p₁ : P) (p₂ : P) :
                            r (p₁ -ᵥ p₂) +ᵥ p₂ affineSpan k {p₁, p₂}

                            A multiple of the difference of two points added to the second point lies in their affine span.

                            theorem vadd_left_mem_affineSpan_pair {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {p₁ : P} {p₂ : P} {v : V} :
                            v +ᵥ p₁ affineSpan k {p₁, p₂} ∃ (r : k), r (p₂ -ᵥ p₁) = v

                            A vector added to the first point lies in the affine span of two points if and only if it is a multiple of their difference.

                            theorem vadd_right_mem_affineSpan_pair {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {p₁ : P} {p₂ : P} {v : V} :
                            v +ᵥ p₂ affineSpan k {p₁, p₂} ∃ (r : k), r (p₁ -ᵥ p₂) = v

                            A vector added to the second point lies in the affine span of two points if and only if it is a multiple of their difference.

                            theorem affineSpan_pair_le_of_mem_of_mem {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {p₁ : P} {p₂ : P} {s : AffineSubspace k P} (hp₁ : p₁ s) (hp₂ : p₂ s) :
                            affineSpan k {p₁, p₂} s

                            The span of two points that lie in an affine subspace is contained in that subspace.

                            theorem affineSpan_pair_le_of_left_mem {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {p₁ : P} {p₂ : P} {p₃ : P} (h : p₁ affineSpan k {p₂, p₃}) :
                            affineSpan k {p₁, p₃} affineSpan k {p₂, p₃}

                            One line is contained in another differing in the first point if the first point of the first line is contained in the second line.

                            theorem affineSpan_pair_le_of_right_mem {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {p₁ : P} {p₂ : P} {p₃ : P} (h : p₁ affineSpan k {p₂, p₃}) :
                            affineSpan k {p₂, p₁} affineSpan k {p₂, p₃}

                            One line is contained in another differing in the second point if the second point of the first line is contained in the second line.

                            theorem affineSpan_mono (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s₁ : Set P} {s₂ : Set P} (h : s₁ s₂) :
                            affineSpan k s₁ affineSpan k s₂

                            affineSpan is monotone.

                            theorem affineSpan_insert_affineSpan (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (p : P) (ps : Set P) :
                            affineSpan k (insert p (affineSpan k ps)) = affineSpan k (insert p ps)

                            Taking the affine span of a set, adding a point and taking the span again produces the same results as adding the point to the set and taking the span.

                            theorem affineSpan_insert_eq_affineSpan (k : Type u_1) {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {p : P} {ps : Set P} (h : p affineSpan k ps) :

                            If a point is in the affine span of a set, adding it to that set does not change the affine span.

                            theorem vectorSpan_insert_eq_vectorSpan {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {p : P} {ps : Set P} (h : p affineSpan k ps) :

                            If a point is in the affine span of a set, adding it to that set does not change the vector span.

                            theorem affineSpan_le_toAffineSubspace_span {k : Type u_1} {V : Type u_2} [Ring k] [AddCommGroup V] [Module k V] {s : Set V} :
                            affineSpan k s (Submodule.span k s).toAffineSubspace

                            When the affine space is also a vector space, the affine span is contained within the linear span.

                            theorem affineSpan_subset_span {k : Type u_1} {V : Type u_2} [Ring k] [AddCommGroup V] [Module k V] {s : Set V} :
                            (affineSpan k s) (Submodule.span k s)
                            theorem AffineSubspace.direction_sup {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s1 : AffineSubspace k P} {s2 : AffineSubspace k P} {p1 : P} {p2 : P} (hp1 : p1 s1) (hp2 : p2 s2) :
                            (s1 s2).direction = s1.direction s2.direction Submodule.span k {p2 -ᵥ p1}

                            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.

                            theorem AffineSubspace.direction_affineSpan_insert {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : AffineSubspace k P} {p1 : P} {p2 : P} (hp1 : p1 s) :
                            (affineSpan k (insert p2 s)).direction = Submodule.span k {p2 -ᵥ p1} s.direction

                            The direction of the span of the result of adding a point to a nonempty affine subspace is the sup of the direction of that subspace and of any one difference between that point and a point in the subspace.

                            theorem AffineSubspace.mem_affineSpan_insert_iff {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : AffineSubspace k P} {p1 : P} (hp1 : p1 s) (p2 : P) (p : P) :
                            p affineSpan k (insert p2 s) ∃ (r : k), p0s, p = r (p2 -ᵥ p1) +ᵥ p0

                            Given a point p1 in an affine subspace s, and a point p2, a point p is in the span of s with p2 added if and only if it is a multiple of p2 -ᵥ p1 added to a point in s.

                            @[simp]
                            theorem AffineMap.vectorSpan_image_eq_submodule_map {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) {s : Set P₁} :
                            Submodule.map f.linear (vectorSpan k s) = vectorSpan k (f '' s)
                            def AffineSubspace.map {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) (s : AffineSubspace k P₁) :

                            The image of an affine subspace under an affine map as an affine subspace.

                            Equations
                            Instances For
                              @[simp]
                              theorem AffineSubspace.coe_map {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) (s : AffineSubspace k P₁) :
                              (AffineSubspace.map f s) = f '' s
                              @[simp]
                              theorem AffineSubspace.mem_map {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] {f : P₁ →ᵃ[k] P₂} {x : P₂} {s : AffineSubspace k P₁} :
                              x AffineSubspace.map f s ys, f y = x
                              theorem AffineSubspace.mem_map_of_mem {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) {x : P₁} {s : AffineSubspace k P₁} (h : x s) :
                              @[simp]
                              theorem AffineSubspace.mem_map_iff_mem_of_injective {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] {f : P₁ →ᵃ[k] P₂} {x : P₁} {s : AffineSubspace k P₁} (hf : Function.Injective f) :
                              @[simp]
                              theorem AffineSubspace.map_bot {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) :
                              @[simp]
                              theorem AffineSubspace.map_eq_bot_iff {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) {s : AffineSubspace k P₁} :
                              @[simp]
                              theorem AffineSubspace.map_id {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (s : AffineSubspace k P₁) :
                              theorem AffineSubspace.map_map {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} {V₃ : Type u_6} {P₃ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [AddCommGroup V₃] [Module k V₃] [AddTorsor V₃ P₃] (s : AffineSubspace k P₁) (f : P₁ →ᵃ[k] P₂) (g : P₂ →ᵃ[k] P₃) :
                              @[simp]
                              theorem AffineSubspace.map_direction {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) (s : AffineSubspace k P₁) :
                              (AffineSubspace.map f s).direction = Submodule.map f.linear s.direction
                              theorem AffineSubspace.map_span {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) (s : Set P₁) :
                              @[simp]
                              theorem AffineSubspace.inclusion_linear {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] {S₁ : AffineSubspace k P₁} {S₂ : AffineSubspace k P₁} [Nonempty S₁] [Nonempty S₂] (h : S₁ S₂) :
                              def AffineSubspace.inclusion {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] {S₁ : AffineSubspace k P₁} {S₂ : AffineSubspace k P₁} [Nonempty S₁] [Nonempty S₂] (h : S₁ S₂) :
                              S₁ →ᵃ[k] S₂

                              Affine map from a smaller to a larger subspace of the same space.

                              This is the affine version of Submodule.inclusion.

                              Equations
                              Instances For
                                @[simp]
                                theorem AffineSubspace.coe_inclusion_apply {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] {S₁ : AffineSubspace k P₁} {S₂ : AffineSubspace k P₁} [Nonempty S₁] [Nonempty S₂] (h : S₁ S₂) (x : S₁) :
                                ((AffineSubspace.inclusion h) x) = x
                                @[simp]
                                theorem AffineSubspace.inclusion_rfl {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] {S₁ : AffineSubspace k P₁} [Nonempty S₁] :
                                @[simp]
                                theorem AffineMap.map_top_of_surjective {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) (hf : Function.Surjective f) :
                                theorem AffineMap.span_eq_top_of_surjective {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) {s : Set P₁} (hf : Function.Surjective f) (h : affineSpan k s = ) :
                                affineSpan k (f '' s) =
                                @[simp]
                                theorem AffineEquiv.linear_ofEq {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (S₁ : AffineSubspace k P₁) (S₂ : AffineSubspace k P₁) [Nonempty S₁] [Nonempty S₂] (h : S₁ = S₂) :
                                (AffineEquiv.ofEq S₁ S₂ h).linear = LinearEquiv.ofEq S₁.direction S₂.direction
                                def AffineEquiv.ofEq {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (S₁ : AffineSubspace k P₁) (S₂ : AffineSubspace k P₁) [Nonempty S₁] [Nonempty S₂] (h : S₁ = S₂) :
                                S₁ ≃ᵃ[k] S₂

                                Affine equivalence between two equal affine subspace.

                                This is the affine version of LinearEquiv.ofEq.

                                Equations
                                Instances For
                                  @[simp]
                                  theorem AffineEquiv.coe_ofEq_apply {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (S₁ : AffineSubspace k P₁) (S₂ : AffineSubspace k P₁) [Nonempty S₁] [Nonempty S₂] (h : S₁ = S₂) (x : S₁) :
                                  ((AffineEquiv.ofEq S₁ S₂ h) x) = x
                                  @[simp]
                                  theorem AffineEquiv.ofEq_symm {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (S₁ : AffineSubspace k P₁) (S₂ : AffineSubspace k P₁) [Nonempty S₁] [Nonempty S₂] (h : S₁ = S₂) :
                                  (AffineEquiv.ofEq S₁ S₂ h).symm = AffineEquiv.ofEq S₂ S₁
                                  @[simp]
                                  theorem AffineEquiv.ofEq_rfl {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (S₁ : AffineSubspace k P₁) [Nonempty S₁] :
                                  AffineEquiv.ofEq S₁ S₁ = AffineEquiv.refl k S₁
                                  theorem AffineEquiv.span_eq_top_iff {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] {s : Set P₁} (e : P₁ ≃ᵃ[k] P₂) :
                                  affineSpan k s = affineSpan k (e '' s) =
                                  def AffineSubspace.comap {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) (s : AffineSubspace k P₂) :

                                  The preimage of an affine subspace under an affine map as an affine subspace.

                                  Equations
                                  Instances For
                                    @[simp]
                                    theorem AffineSubspace.coe_comap {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) (s : AffineSubspace k P₂) :
                                    (AffineSubspace.comap f s) = f ⁻¹' s
                                    @[simp]
                                    theorem AffineSubspace.mem_comap {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] {f : P₁ →ᵃ[k] P₂} {x : P₁} {s : AffineSubspace k P₂} :
                                    theorem AffineSubspace.comap_mono {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] {f : P₁ →ᵃ[k] P₂} {s : AffineSubspace k P₂} {t : AffineSubspace k P₂} :
                                    @[simp]
                                    theorem AffineSubspace.comap_top {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] {f : P₁ →ᵃ[k] P₂} :
                                    @[simp]
                                    theorem AffineSubspace.comap_bot {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) :
                                    @[simp]
                                    theorem AffineSubspace.comap_id {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] (s : AffineSubspace k P₁) :
                                    theorem AffineSubspace.comap_comap {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} {V₃ : Type u_6} {P₃ : Type u_7} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [AddCommGroup V₃] [Module k V₃] [AddTorsor V₃ P₃] (s : AffineSubspace k P₃) (f : P₁ →ᵃ[k] P₂) (g : P₂ →ᵃ[k] P₃) :
                                    theorem AffineSubspace.map_le_iff_le_comap {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] {f : P₁ →ᵃ[k] P₂} {s : AffineSubspace k P₁} {t : AffineSubspace k P₂} :
                                    theorem AffineSubspace.gc_map_comap {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) :
                                    theorem AffineSubspace.map_comap_le {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) (s : AffineSubspace k P₂) :
                                    theorem AffineSubspace.le_comap_map {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) (s : AffineSubspace k P₁) :
                                    theorem AffineSubspace.map_sup {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (s : AffineSubspace k P₁) (t : AffineSubspace k P₁) (f : P₁ →ᵃ[k] P₂) :
                                    theorem AffineSubspace.map_iSup {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] {ι : Sort u_8} (f : P₁ →ᵃ[k] P₂) (s : ιAffineSubspace k P₁) :
                                    AffineSubspace.map f (iSup s) = ⨆ (i : ι), AffineSubspace.map f (s i)
                                    theorem AffineSubspace.comap_inf {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (s : AffineSubspace k P₂) (t : AffineSubspace k P₂) (f : P₁ →ᵃ[k] P₂) :
                                    theorem AffineSubspace.comap_supr {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] {ι : Sort u_8} (f : P₁ →ᵃ[k] P₂) (s : ιAffineSubspace k P₂) :
                                    AffineSubspace.comap f (iInf s) = ⨅ (i : ι), AffineSubspace.comap f (s i)
                                    @[simp]
                                    theorem AffineSubspace.comap_symm {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) (s : AffineSubspace k P₁) :
                                    @[simp]
                                    theorem AffineSubspace.map_symm {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) (s : AffineSubspace k P₂) :
                                    theorem AffineSubspace.comap_span {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (f : P₁ ≃ᵃ[k] P₂) (s : Set P₂) :
                                    def AffineSubspace.Parallel {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s₁ : AffineSubspace k P) (s₂ : AffineSubspace k P) :

                                    Two affine subspaces are parallel if one is related to the other by adding the same vector to all points.

                                    Equations
                                    Instances For

                                      Two affine subspaces are parallel if one is related to the other by adding the same vector to all points.

                                      Equations
                                      Instances For
                                        theorem AffineSubspace.Parallel.symm {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s₁ : AffineSubspace k P} {s₂ : AffineSubspace k P} (h : s₁.Parallel s₂) :
                                        s₂.Parallel s₁
                                        theorem AffineSubspace.parallel_comm {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s₁ : AffineSubspace k P} {s₂ : AffineSubspace k P} :
                                        s₁.Parallel s₂ s₂.Parallel s₁
                                        theorem AffineSubspace.Parallel.refl {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : AffineSubspace k P) :
                                        s.Parallel s
                                        theorem AffineSubspace.Parallel.trans {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s₁ : AffineSubspace k P} {s₂ : AffineSubspace k P} {s₃ : AffineSubspace k P} (h₁₂ : s₁.Parallel s₂) (h₂₃ : s₂.Parallel s₃) :
                                        s₁.Parallel s₃
                                        theorem AffineSubspace.Parallel.direction_eq {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s₁ : AffineSubspace k P} {s₂ : AffineSubspace k P} (h : s₁.Parallel s₂) :
                                        s₁.direction = s₂.direction
                                        @[simp]
                                        theorem AffineSubspace.parallel_bot_iff_eq_bot {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : AffineSubspace k P} :
                                        s.Parallel s =
                                        @[simp]
                                        theorem AffineSubspace.bot_parallel_iff_eq_bot {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : AffineSubspace k P} :
                                        .Parallel s s =
                                        theorem AffineSubspace.parallel_iff_direction_eq_and_eq_bot_iff_eq_bot {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s₁ : AffineSubspace k P} {s₂ : AffineSubspace k P} :
                                        s₁.Parallel s₂ s₁.direction = s₂.direction (s₁ = s₂ = )
                                        theorem AffineSubspace.Parallel.vectorSpan_eq {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s₁ : Set P} {s₂ : Set P} (h : (affineSpan k s₁).Parallel (affineSpan k s₂)) :
                                        vectorSpan k s₁ = vectorSpan k s₂
                                        theorem AffineSubspace.affineSpan_parallel_iff_vectorSpan_eq_and_eq_empty_iff_eq_empty {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s₁ : Set P} {s₂ : Set P} :
                                        (affineSpan k s₁).Parallel (affineSpan k s₂) vectorSpan k s₁ = vectorSpan k s₂ (s₁ = s₂ = )
                                        theorem AffineSubspace.affineSpan_pair_parallel_iff_vectorSpan_eq {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {p₁ : P} {p₂ : P} {p₃ : P} {p₄ : P} :
                                        (affineSpan k {p₁, p₂}).Parallel (affineSpan k {p₃, p₄}) vectorSpan k {p₁, p₂} = vectorSpan k {p₃, p₄}