toEquiv_inclusion — Mathlib

English

From f ≤ g, the inclusion composed with g's embedding equals the inclusion composed with f's embedding after applying toEquiv.

Русский

Из f ≤ g следует, что вложение через g после применения toEquiv эквивалентно вложению через f.

LaTeX

$$$ {f,g : M \simeq_p[L] N} (h : f \le g) : g^{\text{toEquiv}} \circ (\text{Substructure.inclusion}) = (\text{Substructure.inclusion}) \circ f^{\text{toEquiv}} $$$

Lean4

theorem toEquiv_inclusion {f g : M ≃ₚ[L] N} (h : f ≤ g) :
    g.toEquiv.toEmbedding.comp (Substructure.inclusion (dom_le_dom h)) =
      (Substructure.inclusion (cod_le_cod h)).comp f.toEquiv.toEmbedding :=
  by
  rw [← (subtype _).comp_inj, subtype_toEquiv_inclusion h]
  ext
  simp

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