inclusion — Mathlib

English

The composition of two inclusions corresponds to the inclusion with the transitive composition of the containment relations.

Русский

Состав включений эквивалентен включению, соответствующему транзитивному включению.

LaTeX

$$inclusion_inclusion : inclusion htu (inclusion hst x) = inclusion (le_trans hst htu) x$$

Lean4

/-- The map `S → T` when `S` is a non-unital subalgebra contained in the non-unital subalgebra `T`.

This is the non-unital subalgebra version of `Submodule.inclusion`, or `Subring.inclusion` -/
def inclusion {S T : NonUnitalSubalgebra R A} (h : S ≤ T) : S →ₙₐ[R] T
    where
  toFun := Set.inclusion h
  map_add' _ _ := rfl
  map_mul' _ _ := rfl
  map_zero' := rfl
  map_smul' _ _ := rfl

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