val_inclusion — Mathlib

English

Inclusion respects nested subalgebras; the composition of inclusions equals the inclusion of the composite relation.

Русский

Включение сохраняет вложение; композиция включений равна включению составного отношения.

LaTeX

$$$\\text{inclusion}_{UT} \\circ \\text{inclusion}_{ST} = \\text{inclusion}_{SU}$$$

Lean4

@[simp]
theorem val_inclusion {S T : NonUnitalStarSubalgebra R A} (h : S ≤ T) (s : S) : (inclusion h s : A) = s :=
  rfl

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