inclusion_trans — Mathlib

English

For subgroupsoids R ≤ S ≤ T, the inclusion from R to T equals the composition of inclusions: inclusion:(R≤T) = inclusion:(R≤S) ∘ inclusion:(S≤T).

Русский

Для R ≤ S ≤ T выполняется равенство включения: inclusion(R≤T) = inclusion(R≤S) ∘ inclusion(S≤T).

LaTeX

$$inclusion (k.trans h) = inclusion k ⋙ inclusion h$$

Lean4

theorem inclusion_trans {R S T : Subgroupoid C} (k : R ≤ S) (h : S ≤ T) :
    inclusion (k.trans h) = inclusion k ⋙ inclusion h :=
  rfl

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