Documentation

Mathlib.Algebra.Order.Nonneg.Lattice

Lattice structures on the type of nonnegative elements #

instance Nonneg.orderBot {α : Type u_1} [Preorder α] {a : α} :
OrderBot { x : α // a x }

This instance uses data fields from Subtype.partialOrder to help type-class inference. The Set.Ici data fields are definitionally equal, but that requires unfolding semireducible definitions, so type-class inference won't see this.

Equations
    theorem Nonneg.bot_eq {α : Type u_1} [Preorder α] {a : α} :
    = a,
    instance Nonneg.noMaxOrder {α : Type u_1} [PartialOrder α] [NoMaxOrder α] {a : α} :
    NoMaxOrder { x : α // a x }
    instance Nonneg.semilatticeSup {α : Type u_1} [SemilatticeSup α] {a : α} :
    Equations
      instance Nonneg.semilatticeInf {α : Type u_1} [SemilatticeInf α] {a : α} :
      Equations
        instance Nonneg.distribLattice {α : Type u_1} [DistribLattice α] {a : α} :
        Equations
          instance Nonneg.instDenselyOrdered {α : Type u_1} [Preorder α] [DenselyOrdered α] {a : α} :
          @[reducible, inline]

          If sSup ∅ ≤ a then {x : α // a ≤ x} is a ConditionallyCompleteLinearOrder.

          Equations
            Instances For
              @[reducible, inline]

              If sSup ∅ ≤ a then {x : α // a ≤ x} is a ConditionallyCompleteLinearOrderBot.

              This instance uses data fields from Subtype.linearOrder to help type-class inference. The Set.Ici data fields are definitionally equal, but that requires unfolding semireducible definitions, so type-class inference won't see this.

              Equations
                Instances For