inclusion — Mathlib

English

If p ≤ p', then q.subtype ∘ inclusion(h) = p.subtype, i.e., the inclusion followed by the subtype is the same as the subtype of p.

Русский

Если p ≤ p', то q.subtype ∘ inclusion(h) = p.subtype, то есть включение с последующим подтипом даёт тот же подтип.

LaTeX

$$q.\\text{subtype} \\circ \\text{inclusion}(h) = p.\\text{subtype}$$

Lean4

/-- If two submodules `p` and `p'` satisfy `p ⊆ p'`, then `inclusion p p'` is the linear map version
of this inclusion. -/
def inclusion (h : p ≤ p') : p →ₗ[R] p' :=
  p.subtype.codRestrict p' fun ⟨_, hx⟩ => h hx

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