Theorems · Definition · order theory

SupBotHomClass.casesOn

{F : Type u_6} →
  {α : Type u_7} →
    {β : Type u_8} →
      [inst : Max α] →
        [inst_1 : Max β] →
          [inst_2 : Bot α] →
            [inst_3 : Bot β] →
              [inst_4 : FunLike F α β] →
                {motive : SupBotHomClass F α β → Sort u} →
                  (t : SupBotHomClass F α β) →
                    ([toSupHomClass : SupHomClass F α β] → (map_bot : ∀ (f : F), f ⊥ = ⊥) → motive ⋯) → motive t

Defined in

Mathlib.Order.Hom.BoundedLattice

Cited by

0 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

MaxMaxBotBotFunLike