bundledInduced — Mathlib

English

A language-level structure on N is bundled together with the induced structure from an equivalence with M.

Русский

Структура на языке объединяется в пакет вместе с индуцированной структурой по отношению к эквивалентности с M.

LaTeX

$$$\text{Bundled}(L\text{-Structure}, N)\;\text{with induced from } e$$$

Lean4

/-- A type bundled with the structure induced by an equivalence. -/
@[simps]
def bundledInduced : CategoryTheory.Bundled.{w'} L.Structure :=
  ⟨N, g.inducedStructure⟩

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