Mathlib.Algebra.Order.Nonneg.Lattice

Nonneg.orderBot instance

[Preorder α] {a : α} : OrderBot { x : α // a ≤ x }

Full source

/-- 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. -/
instance orderBot [Preorder α] {a : α} : OrderBot { x : α // a ≤ x } :=
  { Set.Ici.orderBot with }

Bottom Element in the Subtype of Nonnegative Elements

Informal description

For any preorder $\alpha$ and any element $a \in \alpha$, the subtype $\{x \in \alpha \mid a \leq x\}$ of nonnegative elements (relative to $a$) has a bottom element $\bot$ given by $a$ itself.

Nonneg.bot_eq theorem

[Preorder α] {a : α} : (⊥ : { x : α // a ≤ x }) = ⟨a, le_rfl⟩

Full source

theorem bot_eq [Preorder α] {a : α} : (⊥ : { x : α // a ≤ x }) = ⟨a, le_rfl⟩ :=
  rfl

Bottom Element in Nonnegative Subtype is Canonical

Informal description

For any preorder $\alpha$ and any element $a \in \alpha$, the bottom element $\bot$ of the subtype $\{x \in \alpha \mid a \leq x\}$ is equal to the pair $\langle a, \text{le\_rfl}\rangle$, where $\text{le\_rfl}$ is the proof that $a \leq a$.

Nonneg.noMaxOrder instance

[PartialOrder α] [NoMaxOrder α] {a : α} : NoMaxOrder { x : α // a ≤ x }

Full source

instance noMaxOrder [PartialOrder α] [NoMaxOrder α] {a : α} : NoMaxOrder { x : α // a ≤ x } :=
  show NoMaxOrder (Ici a) by infer_instance

No Maximal Elements in Nonnegative Subtype of a NoMaxOrder

Informal description

For any partially ordered set $\alpha$ with no maximal elements and any element $a \in \alpha$, the subtype $\{x \in \alpha \mid a \leq x\}$ of elements greater than or equal to $a$ also has no maximal elements.

Nonneg.semilatticeSup instance

[SemilatticeSup α] {a : α} : SemilatticeSup { x : α // a ≤ x }

Full source

instance semilatticeSup [SemilatticeSup α] {a : α} : SemilatticeSup { x : α // a ≤ x } :=
  Set.Ici.semilatticeSup

Join-Semilattice Structure on Nonnegative Elements

Informal description

For any element $a$ in a join-semilattice $\alpha$, the set $\{x \in \alpha \mid a \leq x\}$ forms a join-semilattice where the supremum operation is inherited from $\alpha$.

Nonneg.semilatticeInf instance

[SemilatticeInf α] {a : α} : SemilatticeInf { x : α // a ≤ x }

Full source

instance semilatticeInf [SemilatticeInf α] {a : α} : SemilatticeInf { x : α // a ≤ x } :=
  Set.Ici.semilatticeInf

Meet-Semilattice Structure on Nonnegative Elements

Informal description

For any meet-semilattice $\alpha$ and element $a \in \alpha$, the set $\{x \in \alpha \mid a \leq x\}$ of elements greater than or equal to $a$ forms a meet-semilattice where the meet operation is inherited from $\alpha$.

Nonneg.distribLattice instance

[DistribLattice α] {a : α} : DistribLattice { x : α // a ≤ x }

Full source

instance distribLattice [DistribLattice α] {a : α} : DistribLattice { x : α // a ≤ x } :=
  Set.Ici.distribLattice

Distributive Lattice Structure on Nonnegative Elements

Informal description

For any distributive lattice $\alpha$ and element $a \in \alpha$, the set $\{x \in \alpha \mid a \leq x\}$ of elements greater than or equal to $a$ forms a distributive lattice where the join and meet operations are inherited from $\alpha$.

Nonneg.instDenselyOrdered instance

[Preorder α] [DenselyOrdered α] {a : α} : DenselyOrdered { x : α // a ≤ x }

Full source

instance instDenselyOrdered [Preorder α] [DenselyOrdered α] {a : α} :
    DenselyOrdered { x : α // a ≤ x } :=
  show DenselyOrdered (Ici a) from Set.instDenselyOrdered

Dense Order on Upper Closure of an Element in a Densely Ordered Preorder

Informal description

For any preorder $\alpha$ that is densely ordered and any element $a \in \alpha$, the set $\{x \in \alpha \mid a \leq x\}$ is also densely ordered. That is, for any two elements $x, y$ in this set with $x < y$, there exists an element $z$ in the set such that $x < z < y$.

Nonneg.conditionallyCompleteLinearOrder abbrev

[ConditionallyCompleteLinearOrder α] {a : α} : ConditionallyCompleteLinearOrder { x : α // a ≤ x }

Full source

/-- If `sSup ∅ ≤ a` then `{x : α // a ≤ x}` is a `ConditionallyCompleteLinearOrder`. -/
protected noncomputable abbrev conditionallyCompleteLinearOrder [ConditionallyCompleteLinearOrder α]
    {a : α} : ConditionallyCompleteLinearOrder { x : α // a ≤ x } :=
  { @ordConnectedSubsetConditionallyCompleteLinearOrder α (Set.Ici a) _ ⟨⟨a, le_rfl⟩⟩ _ with }

Conditionally Complete Linear Order Structure on Nonnegative Elements

Informal description

Let $\alpha$ be a conditionally complete linear order and let $a \in \alpha$ be an element such that the supremum of the empty set is less than or equal to $a$. Then the subtype $\{x \in \alpha \mid a \leq x\}$ inherits a conditionally complete linear order structure from $\alpha$.

Nonneg.conditionallyCompleteLinearOrderBot abbrev

[ConditionallyCompleteLinearOrder α] (a : α) : ConditionallyCompleteLinearOrderBot { x : α // a ≤ x }

Full source

/-- 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. -/
protected noncomputable abbrev conditionallyCompleteLinearOrderBot
    [ConditionallyCompleteLinearOrder α] (a : α) :
    ConditionallyCompleteLinearOrderBot { x : α // a ≤ x } :=
  { Nonneg.orderBot, Nonneg.conditionallyCompleteLinearOrder with
    csSup_empty := by
      rw [@subset_sSup_def α (Set.Ici a) _ _ ⟨⟨a, le_rfl⟩⟩]; simp [bot_eq] }

Conditionally Complete Linear Order with Bottom on Nonnegative Elements

Informal description

Let $\alpha$ be a conditionally complete linear order and let $a \in \alpha$ be an element such that the supremum of the empty set is less than or equal to $a$. Then the subtype $\{x \in \alpha \mid a \leq x\}$ inherits a conditionally complete linear order with bottom element structure from $\alpha$, where the bottom element is given by $a$ itself.