inclusion_inclusion — Mathlib

English

Inclusion preserves composition: inclusion hKL ∘ inclusion hHK = inclusion (hHK.trans hKL).

Русский

Включение сохраняет композицию: inclusion hKL ∘ inclusion hHK = inclusion (hHK.trans hKL).

LaTeX

$$$$ inclusion(hKL) \\circ inclusion(hHK) = inclusion(hHK \\text{.trans} hKL). $$$$

Lean4

@[simp]
theorem inclusion_inclusion {L : S} (hHK : H ≤ K) (hKL : K ≤ L) (x : H) :
    inclusion hKL (inclusion hHK x) = inclusion (hHK.trans hKL) x :=
  by
  cases x
  rfl

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