Documentation

Mathlib.Algebra.Order.IsBotOne

Typeclasses expressing IsBot 1 and IsBot 0 #

source
class IsBotZeroClass (α : Type u_1) [LE α] [Zero α] :
Prop

A typeclass expressing that the 0 of a type is a bottom element. In a partial OrderBot, this is equivalent to ⊥ = 0.

Instances
    source
    class IsBotOneClass (α : Type u_1) [LE α] [One α] :
    Prop

    A typeclass expressing that the 1 of a type is a bottom element. In a partial OrderBot, this is equivalent to ⊥ = 1.

    Instances
      source
      theorem isBot_one {α : Type u_1} [LE α] [One α] [IsBotOneClass α] :
      IsBot 1
      source
      theorem isBot_zero {α : Type u_1} [LE α] [Zero α] [IsBotZeroClass α] :
      IsBot 0
      source
      @[simp]
      theorem one_le {α : Type u_1} [LE α] [One α] [IsBotOneClass α] {a : α} :
      1 ≤ a
      source
      @[simp]
      theorem zero_le {α : Type u_1} [LE α] [Zero α] [IsBotZeroClass α] {a : α} :
      0 ≤ a
      source
      @[deprecated zero_le (since := "2026-05-27")]
      theorem zero_le' {α : Type u_1} [LE α] [Zero α] [IsBotZeroClass α] {a : α} :
      0 ≤ a

      Alias of zero_le.

      source
      @[instance_reducible]
      def IsBotOneClass.toOrderBot (α : Type u_1) [LE α] [One α] [IsBotOneClass α] :
      OrderBot α

      Create an OrderBot instance, setting 1 as the bottom element.

      Equations
      Instances For
        source
        @[instance_reducible]
        def IsBotZeroClass.toOrderBot (α : Type u_1) [LE α] [Zero α] [IsBotZeroClass α] :
        OrderBot α

        Create an OrderBot instance, setting 0 as the bottom element.

        Equations
        Instances For
          source
          instance instIsBotOneClassProd {α : Type u_1} [LE α] [One α] [IsBotOneClass α] {β : Type u_2} [LE β] [One β] [IsBotOneClass β] :
          IsBotOneClass (α × β)
          source
          instance instIsBotZeroClassSum {α : Type u_1} [LE α] [Zero α] [IsBotZeroClass α] {β : Type u_2} [LE β] [Zero β] [IsBotZeroClass β] :
          IsBotZeroClass (α × β)
          source
          instance instIsBotOneClassForall {ι : Type u_2} {M : ι → Type u_3} [(i : ι) → LE (M i)] [(i : ι) → One (M i)] [∀ (i : ι), IsBotOneClass (M i)] :
          IsBotOneClass ((i : ι) → M i)
          source
          instance instIsBotZeroClassForall {ι : Type u_2} {M : ι → Type u_3} [(i : ι) → LE (M i)] [(i : ι) → Zero (M i)] [∀ (i : ι), IsBotZeroClass (M i)] :
          IsBotZeroClass ((i : ι) → M i)
          source
          @[instance 100]
          instance instZeroLEOneClassOfIsBotZeroClass {α : Type u_1} [LE α] [Zero α] [One α] [IsBotZeroClass α] :
          ZeroLEOneClass α
          source
          @[instance 100]
          instance instIsBotOneClassOfSubsingleton {α : Type u_1} [Preorder α] [One α] [Subsingleton α] :
          IsBotOneClass α
          source
          @[instance 100]
          instance instIsBotZeroClassOfSubsingleton {α : Type u_1} [Preorder α] [Zero α] [Subsingleton α] :
          IsBotZeroClass α
          source
          @[simp]
          theorem not_lt_one {α : Type u_1} {a : α} [Preorder α] [One α] [IsBotOneClass α] :
          ¬a < 1
          source
          @[simp]
          theorem not_lt_zero {α : Type u_1} {a : α} [Preorder α] [Zero α] [IsBotZeroClass α] :
          ¬a < 0
          source
          @[deprecated not_lt_zero (since := "2026-05-07")]
          theorem not_lt_zero' {α : Type u_1} {a : α} [Preorder α] [Zero α] [IsBotZeroClass α] :
          ¬a < 0

          Alias of not_lt_zero.

          source
          theorem one_lt_of_gt {α : Type u_1} {a b : α} [Preorder α] [One α] [IsBotOneClass α] (h : a < b) :
          1 < b
          source
          theorem pos_of_gt {α : Type u_1} {a b : α} [Preorder α] [Zero α] [IsBotZeroClass α] (h : a < b) :
          0 < b
          source
          theorem LT.lt.one_lt {α : Type u_1} {a b : α} [Preorder α] [One α] [IsBotOneClass α] (h : a < b) :
          1 < b

          Alias of one_lt_of_gt.

          source
          theorem LT.lt.pos {α : Type u_1} {a b : α} [Preorder α] [Zero α] [IsBotZeroClass α] (h : a < b) :
          0 < b

          Alias of pos_of_gt.

          source
          theorem ne_one_of_lt {α : Type u_1} {a b : α} [Preorder α] [One α] [IsBotOneClass α] (h : a < b) :
          b ≠ 1
          source
          theorem ne_zero_of_lt {α : Type u_1} {a b : α} [Preorder α] [Zero α] [IsBotZeroClass α] (h : a < b) :
          b ≠ 0
          source
          theorem LT.lt.ne_one {α : Type u_1} {a b : α} [Preorder α] [One α] [IsBotOneClass α] (h : a < b) :
          b ≠ 1

          Alias of ne_one_of_lt.

          source
          theorem LT.lt.ne_zero {α : Type u_1} {a b : α} [Preorder α] [Zero α] [IsBotZeroClass α] (h : a < b) :
          b ≠ 0

          Alias of ne_zero_of_lt.

          source
          theorem bot_eq_one {α : Type u_1} [PartialOrder α] [One α] [IsBotOneClass α] [OrderBot α] :
          ⊥ = 1
          source
          theorem bot_eq_zero {α : Type u_1} [PartialOrder α] [Zero α] [IsBotZeroClass α] [OrderBot α] :
          ⊥ = 0
          source
          @[deprecated bot_eq_zero (since := "2026-05-07")]
          theorem bot_eq_zero'' {α : Type u_1} [PartialOrder α] [Zero α] [IsBotZeroClass α] [OrderBot α] :
          ⊥ = 0

          Alias of bot_eq_zero.

          source
          @[simp]
          theorem le_one_iff_eq_one {α : Type u_1} {a : α} [PartialOrder α] [One α] [IsBotOneClass α] :
          a ≤ 1 ↔ a = 1
          source
          @[simp]
          theorem nonpos_iff_eq_zero {α : Type u_1} {a : α} [PartialOrder α] [Zero α] [IsBotZeroClass α] :
          a ≤ 0 ↔ a = 0
          source
          theorem le_zero_iff {α : Type u_1} {a : α} [PartialOrder α] [Zero α] [IsBotZeroClass α] :
          a ≤ 0 ↔ a = 0

          Alias of nonpos_iff_eq_zero.

          source
          theorem eq_one_of_le_one {α : Type u_1} {a : α} [PartialOrder α] [One α] [IsBotOneClass α] :
          a ≤ 1 → a = 1

          Alias of the forward direction of le_one_iff_eq_one.

          source
          theorem eq_zero_of_nonpos {α : Type u_1} {a : α} [PartialOrder α] [Zero α] [IsBotZeroClass α] :
          a ≤ 0 → a = 0

          Alias of the forward direction of nonpos_iff_eq_zero.

          source
          theorem LE.le.eq_one {α : Type u_1} {a : α} [PartialOrder α] [One α] [IsBotOneClass α] :
          a ≤ 1 → a = 1

          Alias of eq_one_of_le_one.

          Alias of the forward direction of le_one_iff_eq_one.

          source
          theorem LE.le.eq_zero {α : Type u_1} {a : α} [PartialOrder α] [Zero α] [IsBotZeroClass α] :
          a ≤ 0 → a = 0

          Alias of eq_zero_of_nonpos.

          Alias of the forward direction of nonpos_iff_eq_zero.

          source
          theorem one_lt_iff_ne_one {α : Type u_1} {a : α} [PartialOrder α] [One α] [IsBotOneClass α] :
          1 < a ↔ a ≠ 1
          source
          theorem pos_iff_ne_zero {α : Type u_1} {a : α} [PartialOrder α] [Zero α] [IsBotZeroClass α] :
          0 < a ↔ a ≠ 0
          source
          theorem zero_lt_iff {α : Type u_1} {a : α} [PartialOrder α] [Zero α] [IsBotZeroClass α] :
          0 < a ↔ a ≠ 0

          Alias of pos_iff_ne_zero.

          source
          theorem one_lt_of_ne_one {α : Type u_1} {a : α} [PartialOrder α] [One α] [IsBotOneClass α] :
          a ≠ 1 → 1 < a

          Alias of the reverse direction of one_lt_iff_ne_one.

          source
          theorem pos_of_ne_zero {α : Type u_1} {a : α} [PartialOrder α] [Zero α] [IsBotZeroClass α] :
          a ≠ 0 → 0 < a

          Alias of the reverse direction of pos_iff_ne_zero.

          source
          theorem Ne.one_lt {α : Type u_1} {a : α} [PartialOrder α] [One α] [IsBotOneClass α] :
          a ≠ 1 → 1 < a

          Alias of one_lt_of_ne_one.

          Alias of the reverse direction of one_lt_iff_ne_one.

          source
          theorem Ne.pos {α : Type u_1} {a : α} [PartialOrder α] [Zero α] [IsBotZeroClass α] :
          a ≠ 0 → 0 < a

          Alias of pos_of_ne_zero.

          Alias of the reverse direction of pos_iff_ne_zero.

          source
          theorem eq_one_or_one_lt {α : Type u_1} [PartialOrder α] [One α] [IsBotOneClass α] (a : α) :
          a = 1 ∨ 1 < a
          source
          theorem eq_zero_or_pos {α : Type u_1} [PartialOrder α] [Zero α] [IsBotZeroClass α] (a : α) :
          a = 0 ∨ 0 < a
          source
          theorem one_notMem_iff {α : Type u_1} [PartialOrder α] [One α] [IsBotOneClass α] {s : Set α} :
          ¬1 ∈ s ↔ ∀ (x : α), x ∈ s → 1 < x
          source
          theorem zero_notMem_iff {α : Type u_1} [PartialOrder α] [Zero α] [IsBotZeroClass α] {s : Set α} :
          ¬0 ∈ s ↔ ∀ (x : α), x ∈ s → 0 < x
          source
          theorem one_min {α : Type u_1} [LinearOrder α] [One α] [IsBotOneClass α] (a : α) :
          min 1 a = 1
          source
          theorem zero_min {α : Type u_1} [LinearOrder α] [Zero α] [IsBotZeroClass α] (a : α) :
          min 0 a = 0
          source
          theorem min_one {α : Type u_1} [LinearOrder α] [One α] [IsBotOneClass α] (a : α) :
          min a 1 = 1
          source
          theorem min_zero {α : Type u_1} [LinearOrder α] [Zero α] [IsBotZeroClass α] (a : α) :
          min a 0 = 0
          source
          theorem one_max {α : Type u_1} [LinearOrder α] [One α] [IsBotOneClass α] (a : α) :
          max 1 a = a
          source
          theorem zero_max {α : Type u_1} [LinearOrder α] [Zero α] [IsBotZeroClass α] (a : α) :
          max 0 a = a
          source
          theorem max_one {α : Type u_1} [LinearOrder α] [One α] [IsBotOneClass α] (a : α) :
          max a 1 = a
          source
          theorem max_zero {α : Type u_1} [LinearOrder α] [Zero α] [IsBotZeroClass α] (a : α) :
          max a 0 = a
          source
          @[simp]
          theorem max_eq_one {α : Type u_1} [LinearOrder α] [One α] [IsBotOneClass α] {a b : α} :
          max a b = 1 ↔ a = 1 ∧ b = 1
          source
          @[simp]
          theorem max_eq_zero {α : Type u_1} [LinearOrder α] [Zero α] [IsBotZeroClass α] {a b : α} :
          max a b = 0 ↔ a = 0 ∧ b = 0
          source
          @[simp]
          theorem min_eq_one {α : Type u_1} [LinearOrder α] [One α] [IsBotOneClass α] {a b : α} :
          min a b = 1 ↔ a = 1 ∨ b = 1
          source
          @[simp]
          theorem min_eq_zero {α : Type u_1} [LinearOrder α] [Zero α] [IsBotZeroClass α] {a b : α} :
          min a b = 0 ↔ a = 0 ∨ b = 0
          source
          theorem NeZero.of_gt {α : Type u_1} {a b : α} [Zero α] [Preorder α] [IsBotZeroClass α] (h : a < b) :
          NeZero b
          source
          theorem NeZero.pos {α : Type u_1} [Zero α] [PartialOrder α] [IsBotZeroClass α] (a : α) [NeZero a] :
          0 < a
          source
          @[instance 10]
          instance NeZero.of_gt' {α : Type u_1} {a : α} [Zero α] [Preorder α] [IsBotZeroClass α] [One α] [Fact (1 < a)] :
          NeZero a
          source
          theorem NeZero.of_ge {α : Type u_1} {a b : α} [Zero α] [PartialOrder α] [IsBotZeroClass α] [NeZero a] (h : a ≤ b) :
          NeZero b