Constant-structure J-holomorphic maps

This file defines constant-structure J-holomorphic maps: a map between real normed spaces, each carrying a single fixed almost complex structure, is holomorphic at a point when it has a Frechet derivative there and that derivative commutes with the two structures.

Scope: the constant-structure (flat) model only

The predicates here are named IsConstStructureJHolomorphic* on purpose. They fix one almost complex structure J on the source V and one J' on the target W, both constant across the whole space, and ask that df ∘ J = J' ∘ df. This is ordinary several-variable holomorphy read in linear complex coordinates -- the integrable, flat model -- not a genuine J-holomorphic curve.

A genuine J-holomorphic curve u : Σ → M into an almost complex manifold satisfies du ∘ j = J(u(z)) ∘ du, with the target structure J varying along the map, evaluated at the image point u(z). The constant-structure predicate cannot express that: its target structure J' does not depend on the point. This whole IsConstStructureJHolomorphic* family, and the downstream Neg/Transport/Congruence/Prod/Line/energy calculus built on it, therefore lives entirely in the flat model.

The ConstStructure stem is a deliberate reservation: the plain name belongs to the varying-structure predicate TauCeti.IsJHolomorphic (TauCeti.Geometry.Symplectic.JHolomorphic.Varying), which recovers the flat model recorded here for constant structures (TauCeti.isJHolomorphicAt_constStructure_iff), so the two cannot collide or be mistaken for one another.

Main declarations

• IsConstStructureJHolomorphicAt: a map has a complex-linear Frechet derivative at a point.
• IsConstStructureJHolomorphicWithinAt: a map has a complex-linear Frechet derivative within a set.
• IsConstStructureJHolomorphicOn and IsConstStructureJHolomorphic: setwise and global versions.

It also records the immediate differentiability and continuity consequences of these predicates.

Following the HasFDerivWithinAt API it is built on, the within-set predicate shrinks with the set (IsConstStructureJHolomorphicWithinAt.mono) and agrees with the pointwise one on Set.univ (isConstStructureJHolomorphicWithinAt_univ); the setwise IsConstStructureJHolomorphicOn.mono and isConstStructureJHolomorphicOn_univ are read off from those two pointwise facts.

The Cauchy--Riemann equation df ∘ J = J' ∘ df is real-linear in df, so a continuous real-linear map is holomorphic in this sense exactly when it is complex-linear, and such maps are closed under pointwise sums, differences, and real scalar multiples:

• isConstStructureJHolomorphicAt_continuousLinearMap_iff and isConstStructureJHolomorphic_continuousLinearMap_iff: a continuous real-linear map is IsConstStructureJHolomorphic iff it is complex-linear.
• IsConstStructureJHolomorphicAt.add, IsConstStructureJHolomorphicAt.neg, IsConstStructureJHolomorphicAt.sub, IsConstStructureJHolomorphicAt.const_smul and their within-set, setwise, and global analogues.

The convention follows McDuff--Salamon, J-holomorphic Curves and Symplectic Topology, Section 2.1: the Cauchy--Riemann equation is df ∘ J = J' ∘ df.

def TauCeti.IsConstStructureJHolomorphicAt {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (J : AlmostComplexStructure V) (J' : AlmostComplexStructure W) (f : V → W) (x : V) : Prop

A map is constant-structure J-holomorphic at a point if its Frechet derivative exists there and intertwines the source and target almost complex structures.

def TauCeti.IsConstStructureJHolomorphicWithinAt {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (J : AlmostComplexStructure V) (J' : AlmostComplexStructure W) (f : V → W) (s : Set V) (x : V) : Prop

A map is constant-structure J-holomorphic within a set at a point if its Frechet derivative within the set exists there and intertwines the source and target almost complex structures.

def TauCeti.IsConstStructureJHolomorphicOn {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (J : AlmostComplexStructure V) (J' : AlmostComplexStructure W) (f : V → W) (s : Set V) : Prop

A map is constant-structure J-holomorphic on a set if it is constant-structure J-holomorphic within that set at every point of the set.

def TauCeti.IsConstStructureJHolomorphic {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (J : AlmostComplexStructure V) (J' : AlmostComplexStructure W) (f : V → W) : Prop

A globally constant-structure J-holomorphic map is constant-structure J-holomorphic at every point.

theorem TauCeti.isConstStructureJHolomorphicAt_iff {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (J : AlmostComplexStructure V) (J' : AlmostComplexStructure W) (f : V → W) (x : V) : IsConstStructureJHolomorphicAt J J' f x ↔ ∃ (f' : V →L[ℝ] W), HasFDerivAt f f' x ∧ IsComplexLinearMap J J' ↑f'

Restate pointwise constant-structure J-holomorphicity as existence of a complex-linear Frechet derivative.

theorem TauCeti.isConstStructureJHolomorphicWithinAt_iff {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (J : AlmostComplexStructure V) (J' : AlmostComplexStructure W) (f : V → W) (s : Set V) (x : V) : IsConstStructureJHolomorphicWithinAt J J' f s x ↔ ∃ (f' : V →L[ℝ] W), HasFDerivWithinAt f f' s x ∧ IsComplexLinearMap J J' ↑f'

Restate within-set constant-structure J-holomorphicity as existence of a complex-linear Frechet derivative within the set.

theorem TauCeti.isConstStructureJHolomorphicOn_iff {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (J : AlmostComplexStructure V) (J' : AlmostComplexStructure W) (f : V → W) (s : Set V) : IsConstStructureJHolomorphicOn J J' f s ↔ ∀ x ∈ s, ∃ (f' : V →L[ℝ] W), HasFDerivWithinAt f f' s x ∧ IsComplexLinearMap J J' ↑f'

Restate setwise constant-structure J-holomorphicity as the within-set derivative condition at each point of the set.

theorem TauCeti.isConstStructureJHolomorphic_iff {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (J : AlmostComplexStructure V) (J' : AlmostComplexStructure W) (f : V → W) : IsConstStructureJHolomorphic J J' f ↔ ∀ (x : V), ∃ (f' : V →L[ℝ] W), HasFDerivAt f f' x ∧ IsComplexLinearMap J J' ↑f'

Restate global constant-structure J-holomorphicity as the pointwise derivative condition at every point.

theorem TauCeti.isConstStructureJHolomorphicAt_of_hasFDerivAt {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} {x : V} {f' : V →L[ℝ] W} (hf' : HasFDerivAt f f' x) (hlin : IsComplexLinearMap J J' ↑f') : IsConstStructureJHolomorphicAt J J' f x

Build pointwise constant-structure J-holomorphicity from a complex-linear Frechet derivative.

theorem TauCeti.isConstStructureJHolomorphicWithinAt_of_hasFDerivWithinAt {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} {s : Set V} {x : V} {f' : V →L[ℝ] W} (hf' : HasFDerivWithinAt f f' s x) (hlin : IsComplexLinearMap J J' ↑f') : IsConstStructureJHolomorphicWithinAt J J' f s x

Build within-set constant-structure J-holomorphicity from a complex-linear Frechet derivative within the set.

theorem TauCeti.IsConstStructureJHolomorphicOn.isConstStructureJHolomorphicWithinAt {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} {s : Set V} (hf : IsConstStructureJHolomorphicOn J J' f s) {x : V} (hx : x ∈ s) : IsConstStructureJHolomorphicWithinAt J J' f s x

Extract the within-set predicate at a point of a setwise constant-structure J-holomorphic map.

theorem TauCeti.isConstStructureJHolomorphicOn_of_forall {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} {s : Set V} (hf : ∀ x ∈ s, IsConstStructureJHolomorphicWithinAt J J' f s x) : IsConstStructureJHolomorphicOn J J' f s

Build setwise constant-structure J-holomorphicity from its pointwise-within-set form.

theorem TauCeti.IsConstStructureJHolomorphic.isConstStructureJHolomorphicAt {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} (hf : IsConstStructureJHolomorphic J J' f) (x : V) : IsConstStructureJHolomorphicAt J J' f x

Extract pointwise constant-structure J-holomorphicity from a global one.

theorem TauCeti.isConstStructureJHolomorphic_of_forall {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} (hf : ∀ (x : V), IsConstStructureJHolomorphicAt J J' f x) : IsConstStructureJHolomorphic J J' f

Build global constant-structure J-holomorphicity from its pointwise form.

@[simp]

theorem TauCeti.isConstStructureJHolomorphicWithinAt_univ {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (J : AlmostComplexStructure V) (J' : AlmostComplexStructure W) (f : V → W) (x : V) : IsConstStructureJHolomorphicWithinAt J J' f Set.univ x ↔ IsConstStructureJHolomorphicAt J J' f x

Within the whole space, constant-structure J-holomorphicity is the same as pointwise constant-structure J-holomorphicity.

@[simp]

theorem TauCeti.isConstStructureJHolomorphicOn_univ {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (J : AlmostComplexStructure V) (J' : AlmostComplexStructure W) (f : V → W) : IsConstStructureJHolomorphicOn J J' f Set.univ ↔ IsConstStructureJHolomorphic J J' f

On the whole space, setwise constant-structure J-holomorphicity is the same as global constant-structure J-holomorphicity.

theorem TauCeti.IsConstStructureJHolomorphicAt.hasFDerivAt {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} {x : V} (hf : IsConstStructureJHolomorphicAt J J' f x) : HasFDerivAt f (Classical.choose ⋯) x

The continuous-linear derivative witnessing constant-structure J-holomorphicity at a point.

theorem TauCeti.IsConstStructureJHolomorphicAt.derivative_isComplexLinear {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} {x : V} (hf : IsConstStructureJHolomorphicAt J J' f x) : IsComplexLinearMap J J' ↑(Classical.choose ⋯)

The chosen derivative at a constant-structure J-holomorphic point is complex-linear.

theorem TauCeti.IsConstStructureJHolomorphicAt.differentiableAt {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} {x : V} (hf : IsConstStructureJHolomorphicAt J J' f x) : DifferentiableAt ℝ f x

A constant-structure J-holomorphic map is differentiable at the point.

theorem TauCeti.IsConstStructureJHolomorphicAt.continuousAt {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} {x : V} (hf : IsConstStructureJHolomorphicAt J J' f x) : ContinuousAt f x

A pointwise constant-structure J-holomorphic map is continuous at the point.

theorem TauCeti.IsConstStructureJHolomorphicAt.continuousWithinAt {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} {s : Set V} {x : V} (hf : IsConstStructureJHolomorphicAt J J' f x) : ContinuousWithinAt f s x

A pointwise constant-structure J-holomorphic map is continuous within any source set at the point.

theorem TauCeti.IsConstStructureJHolomorphicAt.fderiv_isComplexLinear {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} {x : V} (hf : IsConstStructureJHolomorphicAt J J' f x) : IsComplexLinearMap J J' ↑(fderiv ℝ f x)

The Frechet derivative of a constant-structure J-holomorphic map is complex-linear.

theorem TauCeti.IsConstStructureJHolomorphicAt.fderiv_apply_commute {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} {x v : V} (hf : IsConstStructureJHolomorphicAt J J' f x) : (fderiv ℝ f x) (J.toLinearMap v) = J'.toLinearMap ((fderiv ℝ f x) v)

The Frechet derivative of a constant-structure J-holomorphic map commutes with the almost complex structures pointwise.

theorem TauCeti.IsConstStructureJHolomorphicAt.isConstStructureJHolomorphicWithinAt {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} {s : Set V} {x : V} (hf : IsConstStructureJHolomorphicAt J J' f x) : IsConstStructureJHolomorphicWithinAt J J' f s x

A pointwise constant-structure J-holomorphic map is constant-structure J-holomorphic within any set.

theorem TauCeti.IsConstStructureJHolomorphicWithinAt.hasFDerivWithinAt {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} {s : Set V} {x : V} (hf : IsConstStructureJHolomorphicWithinAt J J' f s x) : HasFDerivWithinAt f (Classical.choose ⋯) s x

The continuous-linear derivative witnessing constant-structure J-holomorphicity within a set.

theorem TauCeti.IsConstStructureJHolomorphicWithinAt.derivative_isComplexLinear {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} {s : Set V} {x : V} (hf : IsConstStructureJHolomorphicWithinAt J J' f s x) : IsComplexLinearMap J J' ↑(Classical.choose ⋯)

The chosen within-set derivative is complex-linear.

theorem TauCeti.IsConstStructureJHolomorphicWithinAt.mono {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} {s t : Set V} {x : V} (hf : IsConstStructureJHolomorphicWithinAt J J' f t x) (hst : s ⊆ t) : IsConstStructureJHolomorphicWithinAt J J' f s x

Restrict the domain set of a within-set constant-structure J-holomorphic map.

theorem TauCeti.IsConstStructureJHolomorphicWithinAt.differentiableWithinAt {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} {s : Set V} {x : V} (hf : IsConstStructureJHolomorphicWithinAt J J' f s x) : DifferentiableWithinAt ℝ f s x

A map that is constant-structure J-holomorphic within a set is differentiable within that set.

theorem TauCeti.IsConstStructureJHolomorphicWithinAt.continuousWithinAt {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} {s : Set V} {x : V} (hf : IsConstStructureJHolomorphicWithinAt J J' f s x) : ContinuousWithinAt f s x

A map that is constant-structure J-holomorphic within a set is continuous within that set at the point.

theorem TauCeti.IsConstStructureJHolomorphicWithinAt.fderivWithin_isComplexLinear {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} {s : Set V} {x : V} (hf : IsConstStructureJHolomorphicWithinAt J J' f s x) (hs : UniqueDiffWithinAt ℝ s x) : IsComplexLinearMap J J' ↑(fderivWithin ℝ f s x)

The within-set Frechet derivative is complex-linear when the set has unique derivatives.

theorem TauCeti.IsConstStructureJHolomorphicWithinAt.fderivWithin_apply_commute {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} {s : Set V} {x v : V} (hf : IsConstStructureJHolomorphicWithinAt J J' f s x) (hs : UniqueDiffWithinAt ℝ s x) : (fderivWithin ℝ f s x) (J.toLinearMap v) = J'.toLinearMap ((fderivWithin ℝ f s x) v)

The within-set Frechet derivative commutes with the almost complex structures pointwise.

theorem TauCeti.IsConstStructureJHolomorphicWithinAt.isConstStructureJHolomorphicAt_of_mem_nhds {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} {s : Set V} {x : V} (hf : IsConstStructureJHolomorphicWithinAt J J' f s x) (hs : s ∈ nhds x) : IsConstStructureJHolomorphicAt J J' f x

A within-set constant-structure J-holomorphic map is pointwise constant-structure J-holomorphic when the set is a neighborhood of the point.

theorem TauCeti.IsConstStructureJHolomorphicWithinAt.continuousAt_of_mem_nhds {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} {s : Set V} {x : V} (hf : IsConstStructureJHolomorphicWithinAt J J' f s x) (hs : s ∈ nhds x) : ContinuousAt f x

A map that is constant-structure J-holomorphic within a neighborhood of the point is continuous at the point.

theorem TauCeti.IsConstStructureJHolomorphicWithinAt.differentiableAt_of_mem_nhds {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} {s : Set V} {x : V} (hf : IsConstStructureJHolomorphicWithinAt J J' f s x) (hs : s ∈ nhds x) : DifferentiableAt ℝ f x

A map that is constant-structure J-holomorphic within a neighborhood of the point is differentiable at the point.

theorem TauCeti.IsConstStructureJHolomorphicWithinAt.continuousWithinAt_mono {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} {s t : Set V} {x : V} (hf : IsConstStructureJHolomorphicWithinAt J J' f s x) (hts : t ⊆ s) : ContinuousWithinAt f t x

A map that is constant-structure J-holomorphic within a set is continuous within every smaller source set at the point.

@[simp]

theorem TauCeti.isConstStructureJHolomorphicAt_const {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (J : AlmostComplexStructure V) (J' : AlmostComplexStructure W) (c : W) (x : V) : IsConstStructureJHolomorphicAt J J' (fun (x : V) => c) x

A constant map is constant-structure J-holomorphic at every point.

@[simp]

theorem TauCeti.isConstStructureJHolomorphicAt_id {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (J : AlmostComplexStructure V) (x : V) : IsConstStructureJHolomorphicAt J J id x

The identity map is constant-structure J-holomorphic for any fixed almost complex structure J.

@[simp]

theorem TauCeti.isConstStructureJHolomorphicAt_id' {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (J : AlmostComplexStructure V) (x : V) : IsConstStructureJHolomorphicAt J J (fun (y : V) => y) x

Eta-expanded form of isConstStructureJHolomorphicAt_id.

theorem TauCeti.IsConstStructureJHolomorphicAt.comp {V : Type u_1} {W : Type u_2} {X : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] [NormedAddCommGroup X] [NormedSpace ℝ X] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {J'' : AlmostComplexStructure X} {f : V → W} {g : W → X} {x : V} (hg : IsConstStructureJHolomorphicAt J' J'' g (f x)) (hf : IsConstStructureJHolomorphicAt J J' f x) : IsConstStructureJHolomorphicAt J J'' (g ∘ f) x

Chain rule for pointwise constant-structure J-holomorphic maps.

@[simp]

theorem TauCeti.isConstStructureJHolomorphicWithinAt_const {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (J : AlmostComplexStructure V) (J' : AlmostComplexStructure W) (c : W) (s : Set V) (x : V) : IsConstStructureJHolomorphicWithinAt J J' (fun (x : V) => c) s x

A constant map is constant-structure J-holomorphic within every set at every point.

@[simp]

theorem TauCeti.isConstStructureJHolomorphicWithinAt_id {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (J : AlmostComplexStructure V) (s : Set V) (x : V) : IsConstStructureJHolomorphicWithinAt J J id s x

The identity map is constant-structure J-holomorphic within every set at every point.

@[simp]

theorem TauCeti.isConstStructureJHolomorphicWithinAt_id' {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (J : AlmostComplexStructure V) (s : Set V) (x : V) : IsConstStructureJHolomorphicWithinAt J J (fun (y : V) => y) s x

Eta-expanded form of isConstStructureJHolomorphicWithinAt_id.

@[simp]

theorem TauCeti.isConstStructureJHolomorphicOn_const {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (J : AlmostComplexStructure V) (J' : AlmostComplexStructure W) (c : W) (s : Set V) : IsConstStructureJHolomorphicOn J J' (fun (x : V) => c) s

A constant map is constant-structure J-holomorphic on every set.

@[simp]

theorem TauCeti.isConstStructureJHolomorphicOn_id {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (J : AlmostComplexStructure V) (s : Set V) : IsConstStructureJHolomorphicOn J J id s

The identity map is constant-structure J-holomorphic on every set.

@[simp]

theorem TauCeti.isConstStructureJHolomorphicOn_id' {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (J : AlmostComplexStructure V) (s : Set V) : IsConstStructureJHolomorphicOn J J (fun (y : V) => y) s

Eta-expanded form of isConstStructureJHolomorphicOn_id.

theorem TauCeti.IsConstStructureJHolomorphicWithinAt.comp {V : Type u_1} {W : Type u_2} {X : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] [NormedAddCommGroup X] [NormedSpace ℝ X] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {J'' : AlmostComplexStructure X} {f : V → W} {g : W → X} {s : Set V} {t : Set W} {x : V} (hg : IsConstStructureJHolomorphicWithinAt J' J'' g t (f x)) (hf : IsConstStructureJHolomorphicWithinAt J J' f s x) (hst : Set.MapsTo f s t) : IsConstStructureJHolomorphicWithinAt J J'' (g ∘ f) s x

Chain rule for within-set constant-structure J-holomorphic maps.

theorem TauCeti.IsConstStructureJHolomorphicOn.comp {V : Type u_1} {W : Type u_2} {X : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] [NormedAddCommGroup X] [NormedSpace ℝ X] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {J'' : AlmostComplexStructure X} {f : V → W} {g : W → X} {s : Set V} {t : Set W} (hg : IsConstStructureJHolomorphicOn J' J'' g t) (hf : IsConstStructureJHolomorphicOn J J' f s) (hst : Set.MapsTo f s t) : IsConstStructureJHolomorphicOn J J'' (g ∘ f) s

Chain rule for setwise constant-structure J-holomorphic maps.

theorem TauCeti.IsConstStructureJHolomorphicOn.mono {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} {s t : Set V} (hf : IsConstStructureJHolomorphicOn J J' f t) (hst : s ⊆ t) : IsConstStructureJHolomorphicOn J J' f s

Restrict the domain set of a setwise constant-structure J-holomorphic map.

theorem TauCeti.IsConstStructureJHolomorphicOn.differentiableOn {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} {s : Set V} (hf : IsConstStructureJHolomorphicOn J J' f s) : DifferentiableOn ℝ f s

A map that is constant-structure J-holomorphic on a set is differentiable on that set.

theorem TauCeti.IsConstStructureJHolomorphicOn.differentiableWithinAt {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} {s : Set V} {x : V} (hf : IsConstStructureJHolomorphicOn J J' f s) (hx : x ∈ s) : DifferentiableWithinAt ℝ f s x

A map that is constant-structure J-holomorphic on a set is differentiable within that set at each of its points.

theorem TauCeti.IsConstStructureJHolomorphicOn.continuousOn {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} {s : Set V} (hf : IsConstStructureJHolomorphicOn J J' f s) : ContinuousOn f s

A map that is constant-structure J-holomorphic on a set is continuous on that set.

theorem TauCeti.IsConstStructureJHolomorphicOn.continuousWithinAt {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} {s : Set V} {x : V} (hf : IsConstStructureJHolomorphicOn J J' f s) (hx : x ∈ s) : ContinuousWithinAt f s x

A map that is constant-structure J-holomorphic on a set is continuous within that set at each of its points.

theorem TauCeti.IsConstStructureJHolomorphicOn.differentiableAt_of_mem_nhds {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} {s : Set V} {x : V} (hf : IsConstStructureJHolomorphicOn J J' f s) (hs : s ∈ nhds x) : DifferentiableAt ℝ f x

A map that is constant-structure J-holomorphic on a neighborhood of a point is differentiable at that point.

theorem TauCeti.IsConstStructureJHolomorphicOn.continuousAt_of_mem_nhds {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} {s : Set V} {x : V} (hf : IsConstStructureJHolomorphicOn J J' f s) (hs : s ∈ nhds x) : ContinuousAt f x

A map that is constant-structure J-holomorphic on a neighborhood of a point is continuous at that point.

theorem TauCeti.IsConstStructureJHolomorphicOn.differentiableAt_of_isOpen {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} {s : Set V} {x : V} (hf : IsConstStructureJHolomorphicOn J J' f s) (hs : IsOpen s) (hx : x ∈ s) : DifferentiableAt ℝ f x

A map that is constant-structure J-holomorphic on an open set is pointwise differentiable at each point of that set.

theorem TauCeti.IsConstStructureJHolomorphicOn.continuousAt_of_isOpen {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} {s : Set V} {x : V} (hf : IsConstStructureJHolomorphicOn J J' f s) (hs : IsOpen s) (hx : x ∈ s) : ContinuousAt f x

A map that is constant-structure J-holomorphic on an open set is continuous at each point of that set.

theorem TauCeti.IsConstStructureJHolomorphic.isConstStructureJHolomorphicOn {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} (hf : IsConstStructureJHolomorphic J J' f) (s : Set V) : IsConstStructureJHolomorphicOn J J' f s

A globally constant-structure J-holomorphic map is constant-structure J-holomorphic on every set.

theorem TauCeti.IsConstStructureJHolomorphic.differentiable {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} (hf : IsConstStructureJHolomorphic J J' f) : Differentiable ℝ f

A globally constant-structure J-holomorphic map is differentiable.

theorem TauCeti.IsConstStructureJHolomorphic.differentiableAt {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} (hf : IsConstStructureJHolomorphic J J' f) (x : V) : DifferentiableAt ℝ f x

A globally constant-structure J-holomorphic map is differentiable at every point.

theorem TauCeti.IsConstStructureJHolomorphic.continuous {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} (hf : IsConstStructureJHolomorphic J J' f) : Continuous f

A globally constant-structure J-holomorphic map is continuous.

theorem TauCeti.IsConstStructureJHolomorphic.continuousAt {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} (hf : IsConstStructureJHolomorphic J J' f) (x : V) : ContinuousAt f x

A globally constant-structure J-holomorphic map is continuous at every point.

theorem TauCeti.IsConstStructureJHolomorphic.differentiableOn {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} (hf : IsConstStructureJHolomorphic J J' f) (s : Set V) : DifferentiableOn ℝ f s

A globally constant-structure J-holomorphic map is differentiable on every source set.

theorem TauCeti.IsConstStructureJHolomorphic.continuousOn {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} (hf : IsConstStructureJHolomorphic J J' f) (s : Set V) : ContinuousOn f s

A globally constant-structure J-holomorphic map is continuous on every source set.

@[simp]

theorem TauCeti.isConstStructureJHolomorphic_const {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (J : AlmostComplexStructure V) (J' : AlmostComplexStructure W) (c : W) : IsConstStructureJHolomorphic J J' fun (x : V) => c

A constant map is globally constant-structure J-holomorphic.

@[simp]

theorem TauCeti.isConstStructureJHolomorphic_id {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (J : AlmostComplexStructure V) : IsConstStructureJHolomorphic J J id

The identity map is globally constant-structure J-holomorphic.

@[simp]

theorem TauCeti.isConstStructureJHolomorphic_id' {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (J : AlmostComplexStructure V) : IsConstStructureJHolomorphic J J fun (y : V) => y

Eta-expanded form of isConstStructureJHolomorphic_id.

theorem TauCeti.IsConstStructureJHolomorphic.comp {V : Type u_1} {W : Type u_2} {X : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] [NormedAddCommGroup X] [NormedSpace ℝ X] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {J'' : AlmostComplexStructure X} {f : V → W} {g : W → X} (hg : IsConstStructureJHolomorphic J' J'' g) (hf : IsConstStructureJHolomorphic J J' f) : IsConstStructureJHolomorphic J J'' (g ∘ f)

Chain rule for global constant-structure J-holomorphic maps.

theorem TauCeti.isConstStructureJHolomorphicAt_continuousLinearMap_iff {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} (F : V →L[ℝ] W) (x : V) : IsConstStructureJHolomorphicAt J J' (⇑F) x ↔ IsComplexLinearMap J J' ↑F

A continuous real-linear map is constant-structure J-holomorphic at a point iff it is complex-linear: its derivative is the map itself, so the Cauchy--Riemann condition becomes complex-linearity.

theorem TauCeti.isConstStructureJHolomorphic_continuousLinearMap_iff {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} (F : V →L[ℝ] W) : IsConstStructureJHolomorphic J J' ⇑F ↔ IsComplexLinearMap J J' ↑F

A continuous real-linear map is globally constant-structure J-holomorphic iff it is complex-linear.

theorem TauCeti.IsConstStructureJHolomorphicAt.add {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f g : V → W} {x : V} (hf : IsConstStructureJHolomorphicAt J J' f x) (hg : IsConstStructureJHolomorphicAt J J' g x) : IsConstStructureJHolomorphicAt J J' (f + g) x

The pointwise sum of two constant-structure J-holomorphic maps is constant-structure J-holomorphic.

theorem TauCeti.IsConstStructureJHolomorphicAt.neg {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} {x : V} (hf : IsConstStructureJHolomorphicAt J J' f x) : IsConstStructureJHolomorphicAt J J' (-f) x

The pointwise negation of a constant-structure J-holomorphic map is constant-structure J-holomorphic.

theorem TauCeti.IsConstStructureJHolomorphicAt.sub {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f g : V → W} {x : V} (hf : IsConstStructureJHolomorphicAt J J' f x) (hg : IsConstStructureJHolomorphicAt J J' g x) : IsConstStructureJHolomorphicAt J J' (f - g) x

The pointwise difference of two constant-structure J-holomorphic maps is constant-structure J-holomorphic.

theorem TauCeti.IsConstStructureJHolomorphicAt.const_smul {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} {x : V} (hf : IsConstStructureJHolomorphicAt J J' f x) (c : ℝ) : IsConstStructureJHolomorphicAt J J' (c • f) x

A real scalar multiple of a constant-structure J-holomorphic map is constant-structure J-holomorphic.

theorem TauCeti.IsConstStructureJHolomorphicWithinAt.add {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f g : V → W} {s : Set V} {x : V} (hf : IsConstStructureJHolomorphicWithinAt J J' f s x) (hg : IsConstStructureJHolomorphicWithinAt J J' g s x) : IsConstStructureJHolomorphicWithinAt J J' (f + g) s x

The pointwise sum of two maps constant-structure J-holomorphic within a set is constant-structure J-holomorphic within it.

theorem TauCeti.IsConstStructureJHolomorphicWithinAt.neg {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} {s : Set V} {x : V} (hf : IsConstStructureJHolomorphicWithinAt J J' f s x) : IsConstStructureJHolomorphicWithinAt J J' (-f) s x

The pointwise negation of a map constant-structure J-holomorphic within a set is constant-structure J-holomorphic within it.

theorem TauCeti.IsConstStructureJHolomorphicWithinAt.sub {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f g : V → W} {s : Set V} {x : V} (hf : IsConstStructureJHolomorphicWithinAt J J' f s x) (hg : IsConstStructureJHolomorphicWithinAt J J' g s x) : IsConstStructureJHolomorphicWithinAt J J' (f - g) s x

The pointwise difference of two maps constant-structure J-holomorphic within a set is constant-structure J-holomorphic within it.

theorem TauCeti.IsConstStructureJHolomorphicWithinAt.const_smul {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} {s : Set V} {x : V} (hf : IsConstStructureJHolomorphicWithinAt J J' f s x) (c : ℝ) : IsConstStructureJHolomorphicWithinAt J J' (c • f) s x

A real scalar multiple of a map constant-structure J-holomorphic within a set is constant-structure J-holomorphic within it.

theorem TauCeti.IsConstStructureJHolomorphicOn.add {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f g : V → W} {s : Set V} (hf : IsConstStructureJHolomorphicOn J J' f s) (hg : IsConstStructureJHolomorphicOn J J' g s) : IsConstStructureJHolomorphicOn J J' (f + g) s

The pointwise sum of two maps constant-structure J-holomorphic on a set is constant-structure J-holomorphic on it.

theorem TauCeti.IsConstStructureJHolomorphicOn.neg {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} {s : Set V} (hf : IsConstStructureJHolomorphicOn J J' f s) : IsConstStructureJHolomorphicOn J J' (-f) s

The pointwise negation of a map constant-structure J-holomorphic on a set is constant-structure J-holomorphic on it.

theorem TauCeti.IsConstStructureJHolomorphicOn.sub {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f g : V → W} {s : Set V} (hf : IsConstStructureJHolomorphicOn J J' f s) (hg : IsConstStructureJHolomorphicOn J J' g s) : IsConstStructureJHolomorphicOn J J' (f - g) s

The pointwise difference of two maps constant-structure J-holomorphic on a set is constant-structure J-holomorphic on it.

theorem TauCeti.IsConstStructureJHolomorphicOn.const_smul {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} {s : Set V} (hf : IsConstStructureJHolomorphicOn J J' f s) (c : ℝ) : IsConstStructureJHolomorphicOn J J' (c • f) s

A real scalar multiple of a map constant-structure J-holomorphic on a set is constant-structure J-holomorphic on it.

theorem TauCeti.IsConstStructureJHolomorphic.add {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f g : V → W} (hf : IsConstStructureJHolomorphic J J' f) (hg : IsConstStructureJHolomorphic J J' g) : IsConstStructureJHolomorphic J J' (f + g)

The pointwise sum of two globally constant-structure J-holomorphic maps is constant-structure J-holomorphic.

theorem TauCeti.IsConstStructureJHolomorphic.neg {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} (hf : IsConstStructureJHolomorphic J J' f) : IsConstStructureJHolomorphic J J' (-f)

The pointwise negation of a globally constant-structure J-holomorphic map is constant-structure J-holomorphic.

theorem TauCeti.IsConstStructureJHolomorphic.sub {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f g : V → W} (hf : IsConstStructureJHolomorphic J J' f) (hg : IsConstStructureJHolomorphic J J' g) : IsConstStructureJHolomorphic J J' (f - g)

The pointwise difference of two globally constant-structure J-holomorphic maps is constant-structure J-holomorphic.

theorem TauCeti.IsConstStructureJHolomorphic.const_smul {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure V} {J' : AlmostComplexStructure W} {f : V → W} (hf : IsConstStructureJHolomorphic J J' f) (c : ℝ) : IsConstStructureJHolomorphic J J' (c • f)

A real scalar multiple of a globally constant-structure J-holomorphic map is constant-structure J-holomorphic.