inclusion_mk — Mathlib

English

For S ≤ T ≤ U and x ∈ S, the composed inclusions equal the single inclusion S ≤ U applied to x.

Русский

Для S ≤ T ≤ U и x ∈ S композиция включений равна включению S ≤ U на x.

LaTeX

$$\\forall S ≤ T ≤ U,\\; \\forall x ∈ S,\\; inclusion(T)(inclusion(S)(x)) = inclusion(S≤U)(x)$$

Lean4

@[simp]
theorem inclusion_mk {S T : NonUnitalStarSubalgebra R A} (h : S ≤ T) (x : A) (hx : x ∈ S) :
    inclusion h ⟨x, hx⟩ = ⟨x, h hx⟩ :=
  rfl

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