Theorems · Definition · order theory

IsAddQuantale.recOn

{α : Type u_1} →
  [inst : AddSemigroup α] →
    [inst_1 : CompleteLattice α] →
      {motive : IsAddQuantale α → Sort u} →
        (t : IsAddQuantale α) →
          ((add_sSup_distrib : ∀ (x : α) (s : Set α), x + sSup s = ⨆ y ∈ s, x + y) →
              (sSup_add_distrib : ∀ (s : Set α) (y : α), sSup s + y = ⨆ x ∈ s, x + y) → motive ⋯) →
            motive t

Defined in

Mathlib.Algebra.Order.Quantale

Cited by

0 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms

Assumes

AddSemigroupCompleteLattice