ofLE_comp — Mathlib

English

If h12: G1 ≤ G2 and h23: G2 ≤ G3, then the composition of the embeddings of these inclusions equals the embedding from G1 to G3 along the transitive relation: ofLE G2 G3 h23 ∘ ofLE G1 G2 h12 = ofLE G1 G3 (h12.trans h23).

Русский

Если h12: G1 ≤ G2 и h23: G2 ≤ G3, то композиция вложений от G1 в G2 и затем в G3 равна вложению из G1 в G3 по транзитивному отношению: ofLE G2 G3 h23 ∘ ofLE G1 G2 h12 = ofLE G1 G3 (h12.trans h23).

LaTeX

$$$ (ofLE _ _ h_2 3).comp (ofLE _ _ h_1 2) = ofLE _ _ (h_1 2.trans h_2 3) $$$

Lean4

@[simp]
theorem ofLE_comp (h₁₂ : G₁ ≤ G₂) (h₂₃ : G₂ ≤ G₃) : (ofLE _ _ h₂₃).comp (ofLE _ _ h₁₂) = ofLE _ _ (h₁₂.trans h₂₃) := by
  ext; simp

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