subtype_comp_inclusion — Mathlib

English

Same as above: for any p ⊆ p' the equality holds between the two compositions yielding the same subtype.

Русский

То же самое: для любого p ⊆ p' равенство между двумя композициями дает одинаковый подтип.

LaTeX

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

Lean4

theorem subtype_comp_inclusion (p q : Submodule R M) (h : p ≤ q) : q.subtype.comp (inclusion h) = p.subtype :=
  rfl

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