OAI/Topology/CoarseAssembly/IndexFamilyTransport.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Transport of a proved compatible analytic index family

  1. def OAI.CoarseAssembly.Analytic.CompatibleIndexFamily.mapTarget line 18

    Source documentation

    Apply an actual homomorphism to the target of every scale index.

    def mapTarget (I : CompatibleIndexFamily C A) (φ : A →⋆ₙₐ[ℂ] B) :
    CompatibleIndexFamily C B where
…

    Mentions: OAI.CoarseAssembly.Analytic.CompatibleIndexFamily