Lattice structures on the type of nonnegative elements

@[implicit_reducible]

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

Equations

• Nonneg.orderBot = { bot := Nonneg.orderBot._aux_1, bot_le := ⋯ }

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

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

@[implicit_reducible]

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

Equations

• Nonneg.semilatticeSup = { toPartialOrder := Subtype.partialOrder fun (x : α) => a ≤ x, sup := Nonneg.semilatticeSup._aux_1, le_sup_left := ⋯, le_sup_right := ⋯, sup_le := ⋯ }

@[implicit_reducible]

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

Equations

• Nonneg.semilatticeInf = { toPartialOrder := Subtype.partialOrder fun (x : α) => a ≤ x, inf := Nonneg.semilatticeInf._aux_1, inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯ }

@[implicit_reducible]

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

Equations

• Nonneg.distribLattice = { toSemilatticeSup := Nonneg.semilatticeSup, inf := Nonneg.distribLattice._aux_1, inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯, le_sup_inf := ⋯ }

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

• One or more equations did not get rendered due to their size.

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