maximal and minimal elements

def Minimal {α : Type u_1} [PartialOrder α] (a : α) : Prop

Equations

• Minimal a = ∀ (b : α), b ≤ a → b = a

def Maximal {α : Type u_1} [PartialOrder α] (a : α) : Prop

Equations

• Maximal a = ∀ (b : α), a ≤ b → b = a

theorem minimal_iff_no_lt {α : Type u_1} [PartialOrder α] {a : α} : Minimal a ↔ ∀ (b : α), ¬b < a

theorem maximal_iff_no_lt {α : Type u_1} [PartialOrder α] {a : α} : Maximal a ↔ ∀ (b : α), ¬a < b

theorem exists_lt_of_not_maximal {α : Type u_1} [PartialOrder α] {a : α} (h : ¬Maximal a) : ∃ (b : α), a < b

theorem exists_le_of_not_maximal {α : Type u_1} [PartialOrder α] {a : α} (h : ¬Maximal a) : ∃ (b : α), a ≤ b

theorem maximal_toOp_iff_minimal {α : Type u_1} [PartialOrder α] {a : α} : Maximal (toOp a) ↔ Minimal a

theorem minimal_toOp_iff_maximal {α : Type u_1} [PartialOrder α] {a : α} : Minimal (toOp a) ↔ Maximal a

theorem preimage_maximal_strictMono {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {a : α} {f : α → β} (mono : StrictMonotone f) (h : Maximal (f a)) : Maximal a

theorem preimage_minimal_strictMono {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {a : α} {f : α → β} (mono : StrictMonotone f) (h : Minimal (f a)) : Minimal a

theorem preimage_maximal_strictAnti {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {a : α} {f : α → β} (mono : StrictAntitone f) (h : Maximal (f a)) : Minimal a

theorem preimage_minimal_strictAnti {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {a : α} {f : α → β} (mono : StrictAntitone f) (h : Minimal (f a)) : Maximal a

theorem Maximal.subtype {α : Type u_1} [PartialOrder α] {p : α → Prop} {a : { a : α // p a }} (h : Maximal a.val) : Maximal a

theorem Minimal.subtype {α : Type u_1} [PartialOrder α] {p : α → Prop} {a : { a : α // p a }} (h : Minimal a.val) : Minimal a

Greatest and least elements

def Greatest {α : Type u_1} [Preorder α] (a : α) : Prop

Equations

• Greatest a = ∀ (b : α), b ≤ a

def Least {α : Type u_1} [Preorder α] (a : α) : Prop

Equations

• Least a = ∀ (b : α), a ≤ b

theorem greatest_iff_op_least {α : Type u_1} [Preorder α] {a : α} : Greatest a ↔ Least (toOp a)

theorem least_if_op_greatest {α : Type u_1} [Preorder α] {a : α} : Least a ↔ Greatest (toOp a)

theorem Greatest.subtype {α : Type u_1} [Preorder α] {p : α → Prop} {a' : { a : α // p a }} (h : Greatest a'.val) : Greatest a'

theorem Least.subtype {α : Type u_1} [Preorder α] {p : α → Prop} {a' : { a : α // p a }} (h : Least a'.val) : Least a'

theorem Greatest.all_eq {α : Type u_1} [PartialOrder α] {a a' : α} (h : Greatest a) (h' : Greatest a') : a = a'

theorem Least.all_eq {α : Type u_1} [PartialOrder α] {a a' : α} (h : Least a) (h' : Least a') : a = a'

instance instSubsingletonSubtypeGreatest {α : Type u_1} [PartialOrder α] : Subsingleton { a : α // Greatest a }

Equations

• ⋯ = ⋯

instance instSubsingletonSubtypeLeast {α : Type u_1} [PartialOrder α] : Subsingleton { a : α // Least a }

Equations

• ⋯ = ⋯

theorem Greatest.maximal {α : Type u_1} [PartialOrder α] {a : α} (h : Greatest a) : Maximal a

theorem Least.minimal {α : Type u_1} [PartialOrder α] {a : α} (h : Least a) : Minimal a

theorem Greatest.maximal_eq {α : Type u_1} [PartialOrder α] {a a' : α} (h : Greatest a) (h' : Maximal a') : a = a'

theorem Least.minimal_eq {α : Type u_1} [PartialOrder α] {a a' : α} (h : Least a) (h' : Minimal a') : a = a'

def Greatest.unique_maximal {α : Type u_1} [PartialOrder α] {a : α} (h : Greatest a) : Unique { a : α // Maximal a }

Equations

• h.unique_maximal = { default := ⟨a, ⋯⟩, uniq := ⋯ }

def Least.unique_minimal {α : Type u_1} [PartialOrder α] {a : α} (h : Least a) : Unique { a : α // Minimal a }

Equations

• h.unique_minimal = { default := ⟨a, ⋯⟩, uniq := ⋯ }

theorem Monotone.greatest_surj {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {a : α} {f : α → β} (h : Monotone f) (h1 : Function.Surjective f) (h2 : Greatest a) : Greatest (f a)

theorem Monotone.least_surj {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {a : α} {f : α → β} (h : Monotone f) (h1 : Function.Surjective f) (h2 : Least a) : Least (f a)

theorem Antitone.greatest_surj {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {a : α} {f : α → β} (h : Antitone f) (h1 : Function.Surjective f) (h2 : Least a) : Greatest (f a)

theorem Antitone.least_surj {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {a : α} {f : α → β} (h : Antitone f) (h1 : Function.Surjective f) (h2 : Greatest a) : Least (f a)

on partial maps

theorem PartialMap.maximal_iff {α : Type u_1} {β : α → Type u_2} [∀ (a : α), Nonempty (β a)] {x : PartialMap α β} : Maximal x ↔ x.carrier = Set.univ

theorem PartialMap.least_iff {α : Type u_1} {β : α → Type u_2} {x : PartialMap α β} : Least x ↔ x.carrier = ∅

def AdjoinGreatest (α : Type u_3) : Type u_3

Equations

• AdjoinGreatest α = (α ⊕ Unit)

def AdjoinGreatest.to {α : Type u_1} : α → AdjoinGreatest α

Equations

• AdjoinGreatest.to = Sum.inl

def AdjoinGreatest.greatest {α : Type u_1} : AdjoinGreatest α

Equations

• AdjoinGreatest.greatest = Sum.inr ()

instance instLEAdjoinGreatest {α : Type u_1} [LE α] : LE (AdjoinGreatest α)

Equations

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

@[simp]

theorem AdjoinGreatest.le_greatest {α : Type u_1} [LE α] {x : AdjoinGreatest α} : x ≤ AdjoinGreatest.greatest

@[simp]

theorem AdjoinGreatest.to_le_to_iff {α : Type u_1} [LE α] {a b : α} : AdjoinGreatest.to a ≤ AdjoinGreatest.to b ↔ a ≤ b

instance instPreorderAdjoinGreatest {α : Type u_1} [Preorder α] : Preorder (AdjoinGreatest α)

Equations

• instPreorderAdjoinGreatest = Preorder.mk ⋯ ⋯ ⋯

instance instPartialOrderAdjoinGreatest {α : Type u_1} [PartialOrder α] : PartialOrder (AdjoinGreatest α)

Equations

• instPartialOrderAdjoinGreatest = PartialOrder.mk ⋯

@[simp]

theorem AdjoinGreatest.greatest_is_greatest {α : Type u_1} [Preorder α] : Greatest AdjoinGreatest.greatest

def AdjoinLeast (α : Type u_3) : Type u_3

Equations

• AdjoinLeast α = Op (AdjoinGreatest (Op α))

instance instLEAdjoinLeast {α : Type u_1} [LE α] : LE (AdjoinLeast α)

Equations

• instLEAdjoinLeast = id inferInstance

instance instPreorderAdjoinLeast {α : Type u_1} [Preorder α] : Preorder (AdjoinLeast α)

Equations

• instPreorderAdjoinLeast = id inferInstance

instance instPartialOrderAdjoinLeast {α : Type u_1} [PartialOrder α] : PartialOrder (AdjoinLeast α)

Equations

• instPartialOrderAdjoinLeast = id inferInstance

def AdjoinLeast.to {α : Type u_1} : α → AdjoinLeast α

Equations

• AdjoinLeast.to = Sum.inl

def AdjoinLeast.least {α : Type u_1} : AdjoinLeast α

Equations

• AdjoinLeast.least = Sum.inr ()

@[simp]

theorem AdjoinLeast.least_le {α : Type u_1} [LE α] {x : AdjoinLeast α} : AdjoinLeast.least ≤ x

@[simp]

theorem AdjoinLeast.to_le_to_iff {α : Type u_1} [LE α] {a b : α} : AdjoinLeast.to a ≤ AdjoinLeast.to b ↔ a ≤ b

@[simp]

theorem AdjoinLeast.least_is_least {α : Type u_1} [Preorder α] : Least AdjoinLeast.least

@[simp]

theorem greatest_singleton {α : Type u_1} [Preorder α] {a : α} : Greatest ⟨a, ⋯⟩

@[simp]

theorem least_singleton {α : Type u_1} [Preorder α] {a : α} : Least ⟨a, ⋯⟩

class HasLeast (α : Type u_3) [Preorder α] : Type u_3

• least : α
• least_le : ∀ (x : α), ⊥ ≤ x

class HasGreatest (α : Type u_3) [Preorder α] : Type u_3

• greatest : α
• le_greatest : ∀ (x : α), x ≤ ⊤

def «term⊤» : Lean.ParserDescr

The top (⊤, \top) element

Equations

• «term⊤» = Lean.ParserDescr.node `«term⊤» 1024 (Lean.ParserDescr.symbol "⊤")

def «term⊥» : Lean.ParserDescr

The bot (⊥, \bot) element

Equations

• «term⊥» = Lean.ParserDescr.node `«term⊥» 1024 (Lean.ParserDescr.symbol "⊥")

@[instance 100]

instance greatest_nonempty (α : Type u_3) [Preorder α] [HasGreatest α] : Nonempty α

Equations

• ⋯ = ⋯

@[instance 100]

instance least_nonempty (α : Type u_3) [Preorder α] [HasLeast α] : Nonempty α

Equations

• ⋯ = ⋯

@[simp]

theorem least_le {α : Type u_1} [Preorder α] [HasLeast α] (x : α) : ⊥ ≤ x

@[simp]

theorem le_greatest {α : Type u_1} [Preorder α] [HasGreatest α] (x : α) : x ≤ ⊤

theorem least_least {α : Type u_1} [Preorder α] [HasLeast α] : Least ⊥

theorem greatest_greatest {α : Type u_1} [Preorder α] [HasGreatest α] : Greatest ⊤

@[simp]

theorem le_least_iff {α : Type u_1} [PartialOrder α] [HasLeast α] {x : α} : x ≤ ⊥ ↔ x = ⊥

@[simp]

theorem greatest_le_iff {α : Type u_1} [PartialOrder α] [HasGreatest α] {x : α} : ⊤ ≤ x ↔ x = ⊤

@[simp]

theorem ne_least_iff {α : Type u_1} [PartialOrder α] [HasLeast α] {x : α} : x ≠ ⊥ ↔ ⊥ < x

@[simp]

theorem ne_greatest_iff {α : Type u_1} [PartialOrder α] [HasGreatest α] {x : α} : x ≠ ⊤ ↔ x < ⊤

@[simp]

theorem IsOrderIso.greatest {α : Type u_1} {β : Type u_3} [PartialOrder α] [PartialOrder β] [HasGreatest α] [HasGreatest β] {f : α → β} (h : IsOrderIso f) : f ⊤ = ⊤

@[simp]

theorem IsOrderIso.least {α : Type u_1} {β : Type u_3} [PartialOrder α] [PartialOrder β] [HasLeast α] [HasLeast β] {f : α → β} (h : IsOrderIso f) : f ⊥ = ⊥

instance instHasLeastAdjoinLeast {α : Type u_1} [Preorder α] : HasLeast (AdjoinLeast α)

Equations

• instHasLeastAdjoinLeast = { least := AdjoinLeast.least, least_le := ⋯ }

instance instHasGreatestAdjoinGreatest {α : Type u_1} [Preorder α] : HasGreatest (AdjoinGreatest α)

Equations

• instHasGreatestAdjoinGreatest = { greatest := AdjoinGreatest.greatest, le_greatest := ⋯ }

instance instHasGreatestOpOfHasLeast {α : Type u_1} [Preorder α] [HasLeast α] : HasGreatest (Op α)

Equations

• instHasGreatestOpOfHasLeast = { greatest := ⊥, le_greatest := ⋯ }

instance instHasLeastOpOfHasGreatest {α : Type u_1} [Preorder α] [HasGreatest α] : HasLeast (Op α)

Equations

• instHasLeastOpOfHasGreatest = { least := ⊤, least_le := ⋯ }