# Lattice structures on the type of nonnegative elements #

source
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

- Nonneg.orderBot = Set.Ici.orderBot

source
theorem Nonneg.bot_eq {α : Type u_1} [Preorder α] {a : α} :
⊥ = ⟨a, ⋯⟩
source
instance Nonneg.noMaxOrder {α : Type u_1} [PartialOrder α] [NoMaxOrder α] {a : α} :
NoMaxOrder { x : α // a ≤ x }
source
instance Nonneg.semilatticeSup {α : Type u_1} [SemilatticeSup α] {a : α} :
SemilatticeSup { x : α // a ≤ x }
Equations

- Nonneg.semilatticeSup = Set.Ici.semilatticeSup

source
instance Nonneg.semilatticeInf {α : Type u_1} [SemilatticeInf α] {a : α} :
SemilatticeInf { x : α // a ≤ x }
Equations

- Nonneg.semilatticeInf = Set.Ici.semilatticeInf

source
instance Nonneg.distribLattice {α : Type u_1} [DistribLattice α] {a : α} :
DistribLattice { x : α // a ≤ x }
Equations

- Nonneg.distribLattice = Set.Ici.distribLattice

source
instance Nonneg.instDenselyOrdered {α : Type u_1} [Preorder α] [DenselyOrdered α] {a : α} :
DenselyOrdered { x : α // a ≤ x }
source
@[reducible, inline]
noncomputable abbrev Nonneg.conditionallyCompleteLinearOrder {α : Type u_1} [ConditionallyCompleteLinearOrder α] {a : α} :
ConditionallyCompleteLinearOrder { x : α // a ≤ x }

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

Equations

- Nonneg.conditionallyCompleteLinearOrder = ordConnectedSubsetConditionallyCompleteLinearOrder (Set.Ici a)

Instances For

source
@[reducible, inline]
noncomputable abbrev Nonneg.conditionallyCompleteLinearOrderBot {α : Type u_1} [ConditionallyCompleteLinearOrder α] (a : α) :
ConditionallyCompleteLinearOrderBot { x : α // a ≤ x }

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

- Nonneg.conditionallyCompleteLinearOrderBot a = { toConditionallyCompleteLinearOrder := Nonneg.conditionallyCompleteLinearOrder, toOrderBot := Nonneg.orderBot, csSup_empty := ⋯ }

Instances For