Theorems · Definition · order theory

IsQuantale.recOn

{α : Type u_1} →
  [inst : Semigroup α] →
    [inst_1 : CompleteLattice α] →
      {motive : IsQuantale α → Sort u} →
        (t : IsQuantale α) →
          ((mul_sSup_distrib : ∀ (x : α) (s : Set α), x * sSup s = ⨆ y ∈ s, x * y) →
              (sSup_mul_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

SemigroupCompleteLattice