toEquiv_inclusion_apply — Mathlib

English

For h ≤, applying g's toEquiv to an element after inclusion equals applying f's toEquiv to the element after inclusion.

Русский

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

LaTeX

$$$ \forall x \in f.dom, g.toEquiv (Substructure.inclusion (dom\leq dom h) x) = Substructure.inclusion (cod\leq cod h) (f.toEquiv x) $$$

Lean4

theorem toEquiv_inclusion_apply {f g : M ≃ₚ[L] N} (h : f ≤ g) (x : f.dom) :
    g.toEquiv (Substructure.inclusion (dom_le_dom h) x) = Substructure.inclusion (cod_le_cod h) (f.toEquiv x) :=
  by
  apply (subtype _).injective
  change (subtype _).comp (g.toEquiv.toEmbedding.comp (inclusion _)) x = _
  rw [subtype_toEquiv_inclusion h]
  simp

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