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

• Nonneg.orderBot = Set.Ici.orderBot

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 : α} : SemilatticeSup { x : α // a ≤ x }

Equations

• Nonneg.semilatticeSup = Set.Ici.semilatticeSup

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

Equations

• Nonneg.semilatticeInf = Set.Ici.semilatticeInf

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

Equations

• Nonneg.distribLattice = Set.Ici.distribLattice

instance Nonneg.instDenselyOrdered {α : Type u_1} [Preorder α] [DenselyOrdered α] {a : α} : DenselyOrdered { x : α // a ≤ x }

@[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)

@[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 := ⋯ }