inclusion_inclusion — Mathlib

English

Let S ⊆ T ⊆ U be subalgebras of A over R. Then the inclusion maps satisfy i_{T,U} ∘ i_{S,T} = i_{S,U} as maps S → U. In particular, for every x ∈ S, i_{T,U}(i_{S,T}(x)) = i_{S,U}(x).

Русский

Пусть S ⊆ T ⊆ U — подпалгебры A над R. Тогда отображения включения удовлетворяют i_{T,U} ∘ i_{S,T} = i_{S,U} как отображения S → U. Эквивалентно, для каждого x ∈ S выполняется i_{T,U}(i_{S,T}(x)) = i_{S,U}(x).

LaTeX

$$$\forall x \in S,\ (\iota_{T,U}(\iota_{S,T}(x)) = \iota_{S,U}(x))$$$

Lean4

@[simp]
theorem inclusion_inclusion (hst : S ≤ T) (htu : T ≤ U) (x : S) :
    inclusion htu (inclusion hst x) = inclusion (le_trans hst htu) x :=
  Subtype.ext rfl

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