instStrictConvexSpace — Mathlib

English

A subspace (submodule) of a strictly convex space is itself strictly convex.

Русский

Любое подпространство strictly выпуклого пространства по сути также строго выпукло.

LaTeX

$$$[\\text{StrictConvexSpace}_{\\mathbb{K}}(E)] \\Rightarrow [\\text{StrictConvexSpace}_{\\mathbb{K}}(P)]$ для любого подпространства $P\\le E$.$$

Lean4

/-- A vector subspace of a strict convex space is a strict convex space.

This instance has priority 900
to make sure that instances like `LinearIsometry.strictConvexSpace_range`
are tried before this one. -/
instance (priority := 900) instStrictConvexSpace [StrictConvexSpace 𝕜 E] (p : Submodule 𝕜 E) : StrictConvexSpace 𝕜 p :=
  p.subtypeₗᵢ.strictConvexSpace

Похожие утверждения