Theorems · Definition · ring theory

Graded.subtypeMap

{F : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      {σ : Type u_4} →
        {τ : Type u_5} →
          {ι : Type u_6} →
            [inst : SetLike σ A] →
              [inst_1 : SetLike τ B] →
                {𝒜 : ι → σ} →
                  {ℬ : ι → τ} → [inst_2 : FunLike F A B] → [GradedFunLike F 𝒜 ℬ] → F → (i : ι) → ↥(𝒜 i) → ↥(ℬ i)

A graded map descends to a map on each component.

Defined in

Mathlib.Data.FunLike.Graded

Cited by

1 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms

Assumes

SetLikeSetLikeFunLikeGradedFunLike