bundledInducedEquiv — Mathlib

English

A bijection e gives an equivalence between the original type M and the bundled induced structure on N.

Русский

Биекция задаёт эквиваленцию между M и объединённой индуцированной структурой на N.

LaTeX

$$$M \equiv_{L} (g.\text{bundledInduced } L)$$$

Lean4

/-- An equivalence of types as a first-order equivalence to the bundled structure on the codomain.
-/
@[simp]
def bundledInducedEquiv : M ≃[L] g.bundledInduced L :=
  g.inducedStructureEquiv

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