inclusion_inclusion — Mathlib

English

The composition of inclusions along a chain equals the inclusion corresponding to the transitive closure.

Русский

Составления включения вдоль цепи равен включению, соответствующему транзитивному замыканию.

LaTeX

$$inclusion_inclusion : inclusion htu (inclusion hst x) = inclusion (le_trans hst htu) x$$

Lean4

@[simp]
theorem inclusion_inclusion {S T U : NonUnitalSubalgebra R A} (hst : S ≤ T) (htu : T ≤ U) (x : S) :
    inclusion htu (inclusion hst x) = inclusion (le_trans hst htu) x :=
  Subtype.ext rfl

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