inclusion_inclusion — Mathlib

English

For s ⊆ t ⊆ u, the composition of inclusions equals the direct inclusion: inclusion(h t u) o inclusion(h s t) = inclusion(h s t ∘ h t u).

Русский

Для подмножеств s ⊆ t ⊆ 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_inclusion (hst : s ⊆ t) (htu : t ⊆ u) (x : s) :
    inclusion htu (inclusion hst x) = inclusion (hst.trans htu) x :=
  by
  cases x
  rfl

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