subtype_toEquiv_inclusion — Mathlib

English

If f ≤ g then the two composed inclusions with their embeddings coincide as described by subtype inclusions.

Русский

Если f ≤ g, то композиции вложений с их вложениями совпадают в терминах вложений подтипа.

LaTeX

$$$ (subtype _).comp (g.toEquiv.toEmbedding.comp (Substructure.inclusion (dom \leq dom(h)))) = (subtype _).comp f.toEquiv.toEmbedding $$$

Lean4

theorem subtype_toEquiv_inclusion {f g : M ≃ₚ[L] N} (h : f ≤ g) :
    (subtype _).comp (g.toEquiv.toEmbedding.comp (Substructure.inclusion (dom_le_dom h))) =
      (subtype _).comp f.toEquiv.toEmbedding :=
  by let ⟨_, eq⟩ := h; exact eq

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