inducedStructureEquiv — Mathlib

English

The induced equivalence between M and N is exactly the given bijection e.

Русский

Индуцированная эквивалентность между M и N совпадает с заданной биекцией e.

LaTeX

$$$\operatorname{inducedStructureEquiv}(e) = e$$$

Lean4

/-- A bijection as a first-order isomorphism with the induced structure on the codomain. -/
def inducedStructureEquiv (e : M ≃ N) : @Language.Equiv L M N _ (inducedStructure e) :=
  by
  letI : L.Structure N := inducedStructure e
  exact
    { e with
      map_fun' := @fun n f x => by simp [← Function.comp_assoc e.symm e x]
      map_rel' := @fun n r x => by simp [← Function.comp_assoc e.symm e x] }

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