Documentation

Mathlib.LinearAlgebra.AffineSpace.Pointwise

Pointwise instances on AffineSubspaces #

This file provides the additive action AffineSubspace.pointwiseAddAction in the Pointwise locale.

def AffineSubspace.pointwiseAddAction {k : Type u_1} [Ring k] {V : Type u_2} {P : Type u_3} [AddCommGroup V] [Module k V] [AddTorsor V P] :

The additive action on an affine subspace corresponding to applying the action to every element.

This is available as an instance in the Pointwise locale.

Equations
Instances For
    theorem AffineSubspace.pointwise_vadd_eq_map {k : Type u_1} [Ring k] {V : Type u_2} {P : Type u_3} [AddCommGroup V] [Module k V] [AddTorsor V P] (v : V) (s : AffineSubspace k P) :
    @[simp]
    theorem AffineSubspace.coe_pointwise_vadd {k : Type u_1} [Ring k] {V : Type u_2} {P : Type u_3} [AddCommGroup V] [Module k V] [AddTorsor V P] (v : V) (s : AffineSubspace k P) :
    (v +ᵥ s) = v +ᵥ s
    theorem AffineSubspace.vadd_mem_pointwise_vadd_iff {k : Type u_1} [Ring k] {V : Type u_2} {P : Type u_3} [AddCommGroup V] [Module k V] [AddTorsor V P] {v : V} {s : AffineSubspace k P} {p : P} :
    v +ᵥ p v +ᵥ s p s
    @[simp]
    theorem AffineSubspace.pointwise_vadd_bot {k : Type u_1} [Ring k] {V : Type u_2} {P : Type u_3} [AddCommGroup V] [Module k V] [AddTorsor V P] (v : V) :
    @[simp]
    theorem AffineSubspace.pointwise_vadd_top {k : Type u_1} [Ring k] {V : Type u_2} {P : Type u_3} [AddCommGroup V] [Module k V] [AddTorsor V P] (v : V) :
    theorem AffineSubspace.pointwise_vadd_direction {k : Type u_1} [Ring k] {V : Type u_2} {P : Type u_3} [AddCommGroup V] [Module k V] [AddTorsor V P] (v : V) (s : AffineSubspace k P) :
    (v +ᵥ s).direction = s.direction
    theorem AffineSubspace.pointwise_vadd_span {k : Type u_1} [Ring k] {V : Type u_2} {P : Type u_3} [AddCommGroup V] [Module k V] [AddTorsor V P] (v : V) (s : Set P) :
    theorem AffineSubspace.map_pointwise_vadd {k : Type u_1} [Ring k] {V₁ : Type u_4} {P₁ : Type u_5} {V₂ : Type u_6} {P₂ : Type u_7} [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) (v : V₁) (s : AffineSubspace k P₁) :