Theorems · Definition · ring theory

GradedFunLike.casesOn

{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] →
                      {motive : GradedFunLike F 𝒜 ℬ → Sort u} →
                        (t : GradedFunLike F 𝒜 ℬ) →
                          ((map_mem : ∀ (f : F) {i : ι} {x : A}, x ∈ 𝒜 i → f x ∈ ℬ i) → motive ⋯) → motive t

Defined in

Mathlib.Data.FunLike.Graded

Cited by

0 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

SetLikeSetLikeFunLike