inl — Mathlib

English

The left inclusion into a product is an isometry from Q1 to Q1.prod Q2.

Русский

Левое включение в произведение является изометрией от Q1 к Q1.prod Q2.

LaTeX

$$def inl (Q1: QuadraticMap) (Q2: QuadraticMap) : Q1.Isometry (Q1.prod Q2)$$

Lean4

/-- `LinearMap.inl` as an isometry. -/
@[simps!]
def inl (Q₁ : QuadraticMap R M₁ P) (Q₂ : QuadraticMap R M₂ P) : Q₁ →qᵢ (Q₁.prod Q₂)
    where
  toLinearMap := LinearMap.inl R _ _
  map_app' m₁ := by simp

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