Documentation

TauCeti.Analysis.Calculus.DifferentialForm.Plane

Coordinate one-forms on the real plane #

This file defines the constant coordinate one-forms realPlaneDx and realPlaneDy on ℝ × ℝ, together with their exterior derivative identities.

source
def Prod.realPlaneDx :
ℝ × ℝ → (ℝ × ℝ) [⋀^Fin 1]→L[ℝ] ℝ

The constant coordinate one-form dx on ℝ × ℝ.

Instances For
    source
    def Prod.realPlaneDy :
    ℝ × ℝ → (ℝ × ℝ) [⋀^Fin 1]→L[ℝ] ℝ

    The constant coordinate one-form dy on ℝ × ℝ.

    Instances For
      source
      @[simp]
      theorem Prod.realPlaneDx_apply (p : ℝ × ℝ) (v : Fin 1 → ℝ × ℝ) :
      p.realPlaneDx v = (v 0).1

      The coordinate one-form dx evaluates to the first component of its argument.

      source
      @[simp]
      theorem Prod.realPlaneDy_apply (p : ℝ × ℝ) (v : Fin 1 → ℝ × ℝ) :
      p.realPlaneDy v = (v 0).2

      The coordinate one-form dy evaluates to the second component of its argument.

      source
      theorem Prod.contDiff_realPlaneDx {n : WithTop ℕ∞} :
      ContDiff ℝ n realPlaneDx

      The constant coordinate one-form dx is smooth.

      source
      theorem Prod.contDiff_realPlaneDy {n : WithTop ℕ∞} :
      ContDiff ℝ n realPlaneDy

      The constant coordinate one-form dy is smooth.

      source
      theorem Prod.realPlaneDx_eq_const :
      realPlaneDx = fun (x : ℝ × ℝ) => (0, 0).realPlaneDx

      The coordinate one-form dx is independent of its base point.

      source
      theorem Prod.realPlaneDy_eq_const :
      realPlaneDy = fun (x : ℝ × ℝ) => (0, 0).realPlaneDy

      The coordinate one-form dy is independent of its base point.

      source
      @[simp]
      theorem Prod.extDeriv_realPlaneDx (p : ℝ × ℝ) :
      extDeriv realPlaneDx p = 0

      The exterior derivative of the constant coordinate one-form dx vanishes.

      source
      @[simp]
      theorem Prod.extDeriv_realPlaneDy (p : ℝ × ℝ) :
      extDeriv realPlaneDy p = 0

      The exterior derivative of the constant coordinate one-form dy vanishes.