`NRR.Geometry.ConvexBody` — images under continuous linear equivalences #

This module provides an API for images and preimages of ConvexBodys under continuous linear equivalences e : E ≃L[ℝ] F. Only linear equivalences are treated: an arbitrary continuous linear map L : E →L[ℝ] F may be non-injective and collapse the interior, so it never preserves the solidity (interior_nonempty') field of a ConvexBody and is intentionally excluded here (and by module design).

The two constructors are

ConvexBody.imageLinearEquiv K e : ConvexBody F with carrier e '' K;
ConvexBody.preimageLinearEquiv K e : ConvexBody E with carrier e ⁻¹' K (defined as the image under e.symm).

together with carrier/membership simp lemmas, the structural facts (convex, compact, nonempty, nonempty interior), and the identity / composition / inverse laws.

Why no finite-dimensionality hypothesis is needed #

Unlike an AffineEquiv, a ContinuousLinearEquiv bundles continuity of both e and e.symm by definition, and is in particular a homeomorphism via ContinuousLinearEquiv.toHomeomorph. Consequently no finite-dimensionality assumption is required: continuity (for compactness of the image) and openness (for interior preservation) come for free. The declarations below only assume that E, F (and, for composition, G) are real normed spaces.

Mathlib lemmas reused #

ContinuousLinearEquiv.toHomeomorph — a continuous linear equivalence as a homeomorphism.
ContinuousLinearEquiv.coe_toHomeomorph — its underlying function is e.
Homeomorph.image_interior — h '' interior s = interior (h '' s).
Convex.linear_image — linear image of a convex set is convex.
IsCompact.image — continuous image of a compact set is compact.
ContinuousLinearEquiv.image_eq_preimage_symm, ContinuousLinearEquiv.coe_refl, ContinuousLinearEquiv.symm_trans and friends — carrier bookkeeping.

Import policy #

Following the library-wide policy, Basic.lean already pulls in import Mathlib, so no extra imports are required here.

source

theorem NRR.Geometry.ConvexBody.continuousLinearEquiv_image_interior {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (e : E ≃L[ℝ ] F) (s : Set E) :

⇑e '' interior s = interior (⇑e '' s)

A continuous linear equivalence preserves interiors: e '' interior s = interior (e '' s). This is Homeomorph.image_interior transported along ContinuousLinearEquiv.toHomeomorph.

source

def NRR.Geometry.ConvexBody.imageLinearEquiv {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (K : ConvexBody E) (e : E ≃L[ℝ ] F) :

ConvexBody F

The image of a convex body under a continuous linear equivalence, as a convex body with carrier e '' K. Solidity is preserved because a continuous linear equivalence is a homeomorphism.

Equations

K.imageLinearEquiv e = { carrier := ⇑e '' K.carrier, convex' := ⋯, isCompact' := ⋯, interior_nonempty' := ⋯ }

Instances For

source

@[simp]

theorem NRR.Geometry.ConvexBody.imageLinearEquiv_carrier {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (K : ConvexBody E) (e : E ≃L[ℝ ] F) :

(K.imageLinearEquiv e).carrier = ⇑e '' K.carrier

source

theorem NRR.Geometry.ConvexBody.mem_imageLinearEquiv {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (K : ConvexBody E) (e : E ≃L[ℝ ] F) (y : F) :

y ∈ (K.imageLinearEquiv e).carrier ↔ e.symm y ∈ K.carrier

source

def NRR.Geometry.ConvexBody.preimageLinearEquiv {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (K : ConvexBody F) (e : E ≃L[ℝ ] F) :

ConvexBody E

The preimage of a convex body under a continuous linear equivalence, as a convex body with carrier e ⁻¹' K. Implemented as the image under e.symm.

Equations