restrict₂_comp_restrict₂ — Mathlib

English

Restrict₂ respects the transitive restriction: composing two restrict₂ maps yields the single restrict₂ with the transitive subset.

Русский

restrict₂ сохраняет транзитивность ограничений: композиция двух restrict₂ равна restrict₂ от суммы подмножеств.

LaTeX

$$$(restrict₂ hst) \\circ (restrict₂ htu) = restrict₂ (hst.trans htu)$$$

Lean4

theorem restrict₂_comp_restrict₂ {s t u : Set α} (hst : s ⊆ t) (htu : t ⊆ u) :
    (restrict₂ (π := π) hst) ∘ (restrict₂ htu) = restrict₂ (hst.trans htu) :=
  rfl

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