inclusion_comp_inclusion — Mathlib

English

For s ⊆ t and t ⊆ u, the composition of inclusions equals the inclusion from s to u: inclusion htu ∘ inclusion hst = inclusion (hst.trans htu).

Русский

Для s ⊆ t и t ⊆ u композиция включений равна включению из s в u: inclusion htu ∘ inclusion hst = inclusion (hst.trans htu).

LaTeX

$$$\mathrm{inclusion}(htu) \circ \mathrm{inclusion}(hst) = \mathrm{inclusion}(hst \;\mathrm{trans}\; htu).$$$

Lean4

@[simp]
theorem inclusion_comp_inclusion {α} {s t u : Set α} (hst : s ⊆ t) (htu : t ⊆ u) :
    inclusion htu ∘ inclusion hst = inclusion (hst.trans htu) :=
  funext (inclusion_inclusion hst htu)

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