Lattice structures on the type of nonnegative elements

@[instance_reducible]

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

theorem Nonneg.bot_eq {α : Type u_1} [Preorder α] {a : α} : ⊥ = ⟨a, ⋯⟩

instance Nonneg.noMaxOrder {α : Type u_1} [PartialOrder α] [NoMaxOrder α] {a : α} : NoMaxOrder { x : α // a ≤ x }

@[instance_reducible]

instance Nonneg.semilatticeSup {α : Type u_1} [SemilatticeSup α] {a : α} : SemilatticeSup { x : α // a ≤ x }

@[instance_reducible]

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

@[instance_reducible]

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

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.

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