/-
Copyright (c) 2014 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jeremy Avigad, Yury Kudryashov, Yaël Dillies

! This file was ported from Lean 3 source module order.max
! leanprover-community/mathlib commit 6623e6af705e97002a9054c1c05a980180276fc1
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Order.Synonym

/-!
# Minimal/maximal and bottom/top elements

This file defines predicates for elements to be minimal/maximal or bottom/top and typeclasses
saying that there are no such elements.

## Predicates

* `IsBot`: An element is *bottom* if all elements are greater than it.
* `IsTop`: An element is *top* if all elements are less than it.
* `IsMin`: An element is *minimal* if no element is strictly less than it.
* `IsMax`: An element is *maximal* if no element is strictly greater than it.

See also `isBot_iff_isMin` and `isTop_iff_isMax` for the equivalences in a (co)directed order.

## Typeclasses

* `NoBotOrder`: An order without bottom elements.
* `NoTopOrder`: An order without top elements.
* `NoMinOrder`: An order without minimal elements.
* `NoMaxOrder`: An order without maximal elements.
-/


open OrderDual

universe u v

variable {α: Type ?u.7557
α β: Type ?u.42
β : Type _: Type (?u.19004+1)
Type _}

/-- Order without bottom elements. -/
class NoBotOrder: (α : Type u_1) → [inst : LE α] → Prop
NoBotOrder (α: Type ?u.14
α : Type _: Type (?u.14+1)
Type _) [LE: Type ?u.17 → Type ?u.17
LE α: Type ?u.14
α] : Prop: Type
Prop where
  /-- For each term `a`, there is some `b` which is either incomparable or strictly smaller. -/
  exists_not_ge: ∀ {α : Type u_1} [inst : LE α] [self : NoBotOrder α] (a : α), ∃ b, ¬a ≤ b
exists_not_ge (a: α
a : α: Type ?u.14
α) : ∃ b: ?m.26
b, ¬a: α
a ≤ b: ?m.26
b
#align no_bot_order NoBotOrder: (α : Type u_1) → [inst : LE α] → Prop
NoBotOrder

/-- Order without top elements. -/
class NoTopOrder: ∀ {α : Type u_1} [inst : LE α], (∀ (a : α), ∃ b, ¬b ≤ a) → NoTopOrder α
NoTopOrder (α: Type ?u.51
α : Type _: Type (?u.51+1)
Type _) [LE: Type ?u.54 → Type ?u.54
LE α: Type ?u.51
α] : Prop: Type
Prop where
  /-- For each term `a`, there is some `b` which is either incomparable or strictly larger. -/
  exists_not_le: ∀ {α : Type u_1} [inst : LE α] [self : NoTopOrder α] (a : α), ∃ b, ¬b ≤ a
exists_not_le (a: α
a : α: Type ?u.51
α) : ∃ b: ?m.63
b, ¬b: ?m.63
b ≤ a: α
a
#align no_top_order NoTopOrder: (α : Type u_1) → [inst : LE α] → Prop
NoTopOrder

/-- Order without minimal elements. Sometimes called coinitial or dense. -/
class NoMinOrder: (α : Type u_1) → [inst : LT α] → Prop
NoMinOrder (α: Type ?u.88
α : Type _: Type (?u.88+1)
Type _) [LT: Type ?u.91 → Type ?u.91
LT α: Type ?u.88
α] : Prop: Type
Prop where
  /-- For each term `a`, there is some strictly smaller `b`. -/
  exists_lt: ∀ {α : Type u_1} [inst : LT α] [self : NoMinOrder α] (a : α), ∃ b, b < a
exists_lt (a: α
a : α: Type ?u.88
α) : ∃ b: ?m.100
b, b: ?m.100
b < a: α
a
#align no_min_order NoMinOrder: (α : Type u_1) → [inst : LT α] → Prop
NoMinOrder

/-- Order without maximal elements. Sometimes called cofinal. -/
class NoMaxOrder: ∀ {α : Type u_1} [inst : LT α], (∀ (a : α), ∃ b, a < b) → NoMaxOrder α
NoMaxOrder (α: Type ?u.125
α : Type _: Type (?u.125+1)
Type _) [LT: Type ?u.128 → Type ?u.128
LT α: Type ?u.125
α] : Prop: Type
Prop where
  /-- For each term `a`, there is some strictly greater `b`. -/
  exists_gt: ∀ {α : Type u_1} [inst : LT α] [self : NoMaxOrder α] (a : α), ∃ b, a < b
exists_gt (a: α
a : α: Type ?u.125
α) : ∃ b: ?m.137
b, a: α
a < b: ?m.137
b
#align no_max_order NoMaxOrder: (α : Type u_1) → [inst : LT α] → Prop
NoMaxOrder

export NoBotOrder (exists_not_ge)

export NoTopOrder (exists_not_le)

export NoMinOrder (exists_lt)

export NoMaxOrder (exists_gt)

instance nonempty_lt: ∀ [inst : LT α] [inst_1 : NoMinOrder α] (a : α), Nonempty { x // x < a }
nonempty_lt [LT: Type ?u.162 → Type ?u.162
LT α: Type ?u.156
α] [NoMinOrder: (α : Type ?u.165) → [inst : LT α] → Prop
NoMinOrder α: Type ?u.156
α] (a: α
a : α: Type ?u.156
α) : Nonempty: Sort ?u.175 → Prop
Nonempty { x: ?m.179
x // x: ?m.179
x < a: α
a } :=
  nonempty_subtype: ∀ {α : Sort ?u.193} {p : α → Prop}, Nonempty (Subtype p) ↔ ∃ a, p a
nonempty_subtype.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 (exists_lt: ∀ {α : Type ?u.206} [inst : LT α] [self : NoMinOrder α] (a : α), ∃ b, b < a
exists_lt a: α
a)

instance nonempty_gt: ∀ [inst : LT α] [inst_1 : NoMaxOrder α] (a : α), Nonempty { x // a < x }
nonempty_gt [LT: Type ?u.255 → Type ?u.255
LT α: Type ?u.249
α] [NoMaxOrder: (α : Type ?u.258) → [inst : LT α] → Prop
NoMaxOrder α: Type ?u.249
α] (a: α
a : α: Type ?u.249
α) : Nonempty: Sort ?u.268 → Prop
Nonempty { x: ?m.272
x // a: α
a < x: ?m.272
x } :=
  nonempty_subtype: ∀ {α : Sort ?u.286} {p : α → Prop}, Nonempty (Subtype p) ↔ ∃ a, p a
nonempty_subtype.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 (exists_gt: ∀ {α : Type ?u.299} [inst : LT α] [self : NoMaxOrder α] (a : α), ∃ b, a < b
exists_gt a: α
a)

instance OrderDual.noBotOrder: ∀ {α : Type u_1} [inst : LE α] [inst_1 : NoTopOrder α], NoBotOrder αᵒᵈ
OrderDual.noBotOrder [LE: Type ?u.351 → Type ?u.351
LE α: Type ?u.345
α] [NoTopOrder: (α : Type ?u.354) → [inst : LE α] → Prop
NoTopOrder α: Type ?u.345
α] : NoBotOrder: (α : Type ?u.362) → [inst : LE α] → Prop
NoBotOrder α: Type ?u.345
αᵒᵈ :=
  ⟨fun a: ?m.396
a => @exists_not_le: ∀ {α : Type ?u.398} [inst : LE α] [self : NoTopOrder α] (a : α), ∃ b, ¬b ≤ a
exists_not_le α: Type ?u.345
α _ _ a: ?m.396
a⟩
#align order_dual.no_bot_order OrderDual.noBotOrder: ∀ {α : Type u_1} [inst : LE α] [inst_1 : NoTopOrder α], NoBotOrder αᵒᵈ
OrderDual.noBotOrder

instance OrderDual.noTopOrder: ∀ [inst : LE α] [inst_1 : NoBotOrder α], NoTopOrder αᵒᵈ
OrderDual.noTopOrder [LE: Type ?u.452 → Type ?u.452
LE α: Type ?u.446
α] [NoBotOrder: (α : Type ?u.455) → [inst : LE α] → Prop
NoBotOrder α: Type ?u.446
α] : NoTopOrder: (α : Type ?u.463) → [inst : LE α] → Prop
NoTopOrder α: Type ?u.446
αᵒᵈ :=
  ⟨fun a: ?m.497
a => @exists_not_ge: ∀ {α : Type ?u.499} [inst : LE α] [self : NoBotOrder α] (a : α), ∃ b, ¬a ≤ b
exists_not_ge α: Type ?u.446
α _ _ a: ?m.497
a⟩
#align order_dual.no_top_order OrderDual.noTopOrder: ∀ {α : Type u_1} [inst : LE α] [inst_1 : NoBotOrder α], NoTopOrder αᵒᵈ
OrderDual.noTopOrder

instance OrderDual.noMinOrder: ∀ {α : Type u_1} [inst : LT α] [inst_1 : NoMaxOrder α], NoMinOrder αᵒᵈ
OrderDual.noMinOrder [LT: Type ?u.553 → Type ?u.553
LT α: Type ?u.547
α] [NoMaxOrder: (α : Type ?u.556) → [inst : LT α] → Prop
NoMaxOrder α: Type ?u.547
α] : NoMinOrder: (α : Type ?u.564) → [inst : LT α] → Prop
NoMinOrder α: Type ?u.547
αᵒᵈ :=
  ⟨fun a: ?m.594
a => @exists_gt: ∀ {α : Type ?u.596} [inst : LT α] [self : NoMaxOrder α] (a : α), ∃ b, a < b
exists_gt α: Type ?u.547
α _ _ a: ?m.594
a⟩
#align order_dual.no_min_order OrderDual.noMinOrder: ∀ {α : Type u_1} [inst : LT α] [inst_1 : NoMaxOrder α], NoMinOrder αᵒᵈ
OrderDual.noMinOrder

instance OrderDual.noMaxOrder: ∀ {α : Type u_1} [inst : LT α] [inst_1 : NoMinOrder α], NoMaxOrder αᵒᵈ
OrderDual.noMaxOrder [LT: Type ?u.649 → Type ?u.649
LT α: Type ?u.643
α] [NoMinOrder: (α : Type ?u.652) → [inst : LT α] → Prop
NoMinOrder α: Type ?u.643
α] : NoMaxOrder: (α : Type ?u.660) → [inst : LT α] → Prop
NoMaxOrder α: Type ?u.643
αᵒᵈ :=
  ⟨fun a: ?m.690
a => @exists_lt: ∀ {α : Type ?u.692} [inst : LT α] [self : NoMinOrder α] (a : α), ∃ b, b < a
exists_lt α: Type ?u.643
α _ _ a: ?m.690
a⟩
#align order_dual.no_max_order OrderDual.noMaxOrder: ∀ {α : Type u_1} [inst : LT α] [inst_1 : NoMinOrder α], NoMaxOrder αᵒᵈ
OrderDual.noMaxOrder

-- See note [lower instance priority]
instance: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : NoMinOrder α], NoBotOrder α
instance (priority := 100) [Preorder: Type ?u.745 → Type ?u.745
Preorder α: Type ?u.739
α] [NoMinOrder: (α : Type ?u.748) → [inst : LT α] → Prop
NoMinOrder α: Type ?u.739
α] : NoBotOrder: (α : Type ?u.762) → [inst : LE α] → Prop
NoBotOrder α: Type ?u.739
α :=
  ⟨fun a: ?m.795
a => (exists_lt: ∀ {α : Type ?u.797} [inst : LT α] [self : NoMinOrder α] (a : α), ∃ b, b < a
exists_lt a: ?m.795
a).imp: ∀ {α : Sort ?u.809} {p q : α → Prop}, (∀ (a : α), p a → q a) → (∃ a, p a) → ∃ a, q a
imp fun _: ?m.825
_ => not_le_of_lt: ∀ {α : Type ?u.827} [inst : Preorder α] {a b : α}, a < b → ¬b ≤ a
not_le_of_lt⟩

-- See note [lower instance priority]
instance: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : NoMaxOrder α], NoTopOrder α
instance (priority := 100) [Preorder: Type ?u.917 → Type ?u.917
Preorder α: Type ?u.911
α] [NoMaxOrder: (α : Type ?u.920) → [inst : LT α] → Prop
NoMaxOrder α: Type ?u.911
α] : NoTopOrder: (α : Type ?u.934) → [inst : LE α] → Prop
NoTopOrder α: Type ?u.911
α :=
  ⟨fun a: ?m.967
a => (exists_gt: ∀ {α : Type ?u.969} [inst : LT α] [self : NoMaxOrder α] (a : α), ∃ b, a < b
exists_gt a: ?m.967
a).imp: ∀ {α : Sort ?u.981} {p q : α → Prop}, (∀ (a : α), p a → q a) → (∃ a, p a) → ∃ a, q a
imp fun _: ?m.997
_ => not_le_of_lt: ∀ {α : Type ?u.999} [inst : Preorder α] {a b : α}, a < b → ¬b ≤ a
not_le_of_lt⟩

instance noMaxOrder_of_left: ∀ [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : NoMaxOrder α], NoMaxOrder (α × β)
noMaxOrder_of_left [Preorder: Type ?u.1089 → Type ?u.1089
Preorder α: Type ?u.1083
α] [Preorder: Type ?u.1092 → Type ?u.1092
Preorder β: Type ?u.1086
β] [NoMaxOrder: (α : Type ?u.1095) → [inst : LT α] → Prop
NoMaxOrder α: Type ?u.1083
α] : NoMaxOrder: (α : Type ?u.1109) → [inst : LT α] → Prop
NoMaxOrder (α: Type ?u.1083
α × β: Type ?u.1086
β) :=
  ⟨fun ⟨a: α
a, b: β
b⟩ => by
Goals accomplished! 🐙
    α: Type ?u.1083

β: Type ?u.1086

inst✝²: Preorder α

inst✝¹: Preorder β

inst✝: NoMaxOrder α

x✝: α × β

a: α

b: β

∃ b_1, (a, b) < b_1obtain ⟨c, h⟩: ∃ b, a < b
⟨c: α
c⟨c, h⟩: ∃ b, a < b
, h: a < c
h⟨c, h⟩: ∃ b, a < b
⟩ := exists_gt: ∀ {α : Type ?u.1281} [inst : LT α] [self : NoMaxOrder α] (a : α), ∃ b, a < b
exists_gt a: α
aα: Type ?u.1083

β: Type ?u.1086

inst✝²: Preorder α

inst✝¹: Preorder β

inst✝: NoMaxOrder α

x✝: α × β

a: α

b: β

c: α

h: a < c

intro∃ b_1, (a, b) < b_1
    α: Type ?u.1083

β: Type ?u.1086

inst✝²: Preorder α

inst✝¹: Preorder β

inst✝: NoMaxOrder α

x✝: α × β

a: α

b: β

∃ b_1, (a, b) < b_1exact ⟨(c: α
c, b: β
b), Prod.mk_lt_mk_iff_left: ∀ {α : Type ?u.1343} {β : Type ?u.1342} [inst : Preorder α] [inst_1 : Preorder β] {a₁ a₂ : α} {b : β},
  (a₁, b) < (a₂, b) ↔ a₁ < a₂
Prod.mk_lt_mk_iff_left.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 h: a < c
h⟩
Goals accomplished! 🐙⟩
#align no_max_order_of_left noMaxOrder_of_left: ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : NoMaxOrder α], NoMaxOrder (α × β)
noMaxOrder_of_left

instance noMaxOrder_of_right: ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : NoMaxOrder β], NoMaxOrder (α × β)
noMaxOrder_of_right [Preorder: Type ?u.1448 → Type ?u.1448
Preorder α: Type ?u.1442
α] [Preorder: Type ?u.1451 → Type ?u.1451
Preorder β: Type ?u.1445
β] [NoMaxOrder: (α : Type ?u.1454) → [inst : LT α] → Prop
NoMaxOrder β: Type ?u.1445
β] : NoMaxOrder: (α : Type ?u.1468) → [inst : LT α] → Prop
NoMaxOrder (α: Type ?u.1442
α × β: Type ?u.1445
β) :=
  ⟨fun ⟨a: α
a, b: β
b⟩ => by
Goals accomplished! 🐙
    α: Type ?u.1442

β: Type ?u.1445

inst✝²: Preorder α

inst✝¹: Preorder β

inst✝: NoMaxOrder β

x✝: α × β

a: α

b: β

∃ b_1, (a, b) < b_1obtain ⟨c, h⟩: ∃ b_1, b < b_1
⟨c: β
c⟨c, h⟩: ∃ b_1, b < b_1
, h: b < c
h⟨c, h⟩: ∃ b_1, b < b_1
⟩ := exists_gt: ∀ {α : Type ?u.1621} [inst : LT α] [self : NoMaxOrder α] (a : α), ∃ b, a < b
exists_gt b: β
bα: Type ?u.1442

β: Type ?u.1445

inst✝²: Preorder α

inst✝¹: Preorder β

inst✝: NoMaxOrder β

x✝: α × β

a: α

b, c: β

h: b < c

intro∃ b_1, (a, b) < b_1
    α: Type ?u.1442

β: Type ?u.1445

inst✝²: Preorder α

inst✝¹: Preorder β

inst✝: NoMaxOrder β

x✝: α × β

a: α

b: β

∃ b_1, (a, b) < b_1exact ⟨(a: α
a, c: β
c), Prod.mk_lt_mk_iff_right: ∀ {α : Type ?u.1679} {β : Type ?u.1678} [inst : Preorder α] [inst_1 : Preorder β] {a : α} {b₁ b₂ : β},
  (a, b₁) < (a, b₂) ↔ b₁ < b₂
Prod.mk_lt_mk_iff_right.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 h: b < c
h⟩
Goals accomplished! 🐙⟩
#align no_max_order_of_right noMaxOrder_of_right: ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : NoMaxOrder β], NoMaxOrder (α × β)
noMaxOrder_of_right

instance noMinOrder_of_left: ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : NoMinOrder α], NoMinOrder (α × β)
noMinOrder_of_left [Preorder: Type ?u.1784 → Type ?u.1784
Preorder α: Type ?u.1778
α] [Preorder: Type ?u.1787 → Type ?u.1787
Preorder β: Type ?u.1781
β] [NoMinOrder: (α : Type ?u.1790) → [inst : LT α] → Prop
NoMinOrder α: Type ?u.1778
α] : NoMinOrder: (α : Type ?u.1804) → [inst : LT α] → Prop
NoMinOrder (α: Type ?u.1778
α × β: Type ?u.1781
β) :=
  ⟨fun ⟨a: α
a, b: β
b⟩ => by
Goals accomplished! 🐙
    α: Type ?u.1778

β: Type ?u.1781

inst✝²: Preorder α

inst✝¹: Preorder β

inst✝: NoMinOrder α

x✝: α × β

a: α

b: β

∃ b_1, b_1 < (a, b)obtain ⟨c, h⟩: ∃ b, b < a
⟨c: α
c⟨c, h⟩: ∃ b, b < a
, h: c < a
h⟨c, h⟩: ∃ b, b < a
⟩ := exists_lt: ∀ {α : Type ?u.1957} [inst : LT α] [self : NoMinOrder α] (a : α), ∃ b, b < a
exists_lt a: α
aα: Type ?u.1778

β: Type ?u.1781

inst✝²: Preorder α

inst✝¹: Preorder β

inst✝: NoMinOrder α

x✝: α × β

a: α

b: β

c: α

h: c < a

intro∃ b_1, b_1 < (a, b)
    α: Type ?u.1778

β: Type ?u.1781

inst✝²: Preorder α

inst✝¹: Preorder β

inst✝: NoMinOrder α

x✝: α × β

a: α

b: β

∃ b_1, b_1 < (a, b)exact ⟨(c: α
c, b: β
b), Prod.mk_lt_mk_iff_left: ∀ {α : Type ?u.2015} {β : Type ?u.2014} [inst : Preorder α] [inst_1 : Preorder β] {a₁ a₂ : α} {b : β},
  (a₁, b) < (a₂, b) ↔ a₁ < a₂
Prod.mk_lt_mk_iff_left.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 h: c < a
h⟩
Goals accomplished! 🐙⟩
#align no_min_order_of_left noMinOrder_of_left: ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : NoMinOrder α], NoMinOrder (α × β)
noMinOrder_of_left

instance noMinOrder_of_right: ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : NoMinOrder β], NoMinOrder (α × β)
noMinOrder_of_right [Preorder: Type ?u.2120 → Type ?u.2120
Preorder α: Type ?u.2114
α] [Preorder: Type ?u.2123 → Type ?u.2123
Preorder β: Type ?u.2117
β] [NoMinOrder: (α : Type ?u.2126) → [inst : LT α] → Prop
NoMinOrder β: Type ?u.2117
β] : NoMinOrder: (α : Type ?u.2140) → [inst : LT α] → Prop
NoMinOrder (α: Type ?u.2114
α × β: Type ?u.2117
β) :=
  ⟨fun ⟨a: α
a, b: β
b⟩ => by
Goals accomplished! 🐙
    α: Type ?u.2114

β: Type ?u.2117

inst✝²: Preorder α

inst✝¹: Preorder β

inst✝: NoMinOrder β

x✝: α × β

a: α

b: β

∃ b_1, b_1 < (a, b)obtain ⟨c, h⟩: ∃ b_1, b_1 < b
⟨c: β
c⟨c, h⟩: ∃ b_1, b_1 < b
, h: c < b
h⟨c, h⟩: ∃ b_1, b_1 < b
⟩ := exists_lt: ∀ {α : Type ?u.2293} [inst : LT α] [self : NoMinOrder α] (a : α), ∃ b, b < a
exists_lt b: β
bα: Type ?u.2114

β: Type ?u.2117

inst✝²: Preorder α

inst✝¹: Preorder β

inst✝: NoMinOrder β

x✝: α × β

a: α

b, c: β

h: c < b

intro∃ b_1, b_1 < (a, b)
    α: Type ?u.2114

β: Type ?u.2117

inst✝²: Preorder α

inst✝¹: Preorder β

inst✝: NoMinOrder β

x✝: α × β

a: α

b: β

∃ b_1, b_1 < (a, b)exact ⟨(a: α
a, c: β
c), Prod.mk_lt_mk_iff_right: ∀ {α : Type ?u.2351} {β : Type ?u.2350} [inst : Preorder α] [inst_1 : Preorder β] {a : α} {b₁ b₂ : β},
  (a, b₁) < (a, b₂) ↔ b₁ < b₂
Prod.mk_lt_mk_iff_right.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 h: c < b
h⟩
Goals accomplished! 🐙⟩
#align no_min_order_of_right noMinOrder_of_right: ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : NoMinOrder β], NoMinOrder (α × β)
noMinOrder_of_right

instance: ∀ {ι : Type u} {π : ι → Type u_1} [inst : Nonempty ι] [inst : (i : ι) → Preorder (π i)]
  [inst_1 : ∀ (i : ι), NoMaxOrder (π i)], NoMaxOrder ((i : ι) → π i)
instance {ι: Type u
ι : Type u: Type (u+1)
Type u} {π: ι → Type ?u.2460
π : ι: Type u
ι → Type _: Type (?u.2460+1)
Type _} [Nonempty: Sort ?u.2463 → Prop
Nonempty ι: Type u
ι] [∀ i: ?m.2467
i, Preorder: Type ?u.2470 → Type ?u.2470
Preorder (π: ι → Type ?u.2460
π i: ?m.2467
i)] [∀ i: ?m.2475
i, NoMaxOrder: (α : Type ?u.2478) → [inst : LT α] → Prop
NoMaxOrder (π: ι → Type ?u.2460
π i: ?m.2475
i)] :
    NoMaxOrder: (α : Type ?u.2496) → [inst : LT α] → Prop
NoMaxOrder (∀ i: ?m.2498
i, π: ι → Type ?u.2460
π i: ?m.2498
i) :=
  ⟨fun a: ?m.2568
a => by
Goals accomplished! 🐙
    α: Type ?u.2450

β: Type ?u.2453

ι: Type u

π: ι → Type ?u.2460

inst✝²: Nonempty ι

inst✝¹: (i : ι) → Preorder (π i)

inst✝: ∀ (i : ι), NoMaxOrder (π i)

a: (i : ι) → π i

∃ b, a < bclassical
    α: Type ?u.2450

β: Type ?u.2453

ι: Type u

π: ι → Type ?u.2460

inst✝²: Nonempty ι

inst✝¹: (i : ι) → Preorder (π i)

inst✝: ∀ (i : ι), NoMaxOrder (π i)

a: (i : ι) → π i

∃ b, a < bobtain ⟨b, hb⟩: ∃ b, a (Classical.arbitrary ι) < b
⟨b: π (Classical.arbitrary ι)
b⟨b, hb⟩: ∃ b, a (Classical.arbitrary ι) < b
, hb: a (Classical.arbitrary ι) < b
hb⟨b, hb⟩: ∃ b, a (Classical.arbitrary ι) < b
⟩ := exists_gt: ∀ {α : Type ?u.2619} [inst : LT α] [self : NoMaxOrder α] (a : α), ∃ b, a < b
exists_gt (a: (i : ι) → π i
a <| Classical.arbitrary: (α : Sort ?u.2623) → [h : Nonempty α] → α
Classical.arbitrary _: Sort ?u.2623
_)α: Type ?u.2450

β: Type ?u.2453

ι: Type u

π: ι → Type ?u.2460

inst✝²: Nonempty ι

inst✝¹: (i : ι) → Preorder (π i)

inst✝: ∀ (i : ι), NoMaxOrder (π i)

a: (i : ι) → π i

b: π (Classical.arbitrary ι)

hb: a (Classical.arbitrary ι) < b

intro∃ b, a < b
    α: Type ?u.2450

β: Type ?u.2453

ι: Type u

π: ι → Type ?u.2460

inst✝²: Nonempty ι

inst✝¹: (i : ι) → Preorder (π i)

inst✝: ∀ (i : ι), NoMaxOrder (π i)

a: (i : ι) → π i

∃ b, a < bexact ⟨_: ?m.2725
_, lt_update_self_iff: ∀ {ι : Type ?u.2734} {π : ι → Type ?u.2735} [inst : DecidableEq ι] [inst_1 : (i : ι) → Preorder (π i)]
  {x : (i : ι) → π i} {i : ι} {a : π i}, x < Function.update x i a ↔ x i < a
lt_update_self_iff.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 hb: a (Classical.arbitrary ι) < b
hb⟩
Goals accomplished! 🐙⟩

instance: ∀ {ι : Type u} {π : ι → Type u_1} [inst : Nonempty ι] [inst : (i : ι) → Preorder (π i)]
  [inst_1 : ∀ (i : ι), NoMinOrder (π i)], NoMinOrder ((i : ι) → π i)
instance {ι: Type u
ι : Type u: Type (u+1)
Type u} {π: ι → Type ?u.2975
π : ι: Type u
ι → Type _: Type (?u.2975+1)
Type _} [Nonempty: Sort ?u.2978 → Prop
Nonempty ι: Type u
ι] [∀ i: ?m.2982
i, Preorder: Type ?u.2985 → Type ?u.2985
Preorder (π: ι → Type ?u.2975
π i: ?m.2982
i)] [∀ i: ?m.2990
i, NoMinOrder: (α : Type ?u.2993) → [inst : LT α] → Prop
NoMinOrder (π: ι → Type ?u.2975
π i: ?m.2990
i)] :
    NoMinOrder: (α : Type ?u.3011) → [inst : LT α] → Prop
NoMinOrder (∀ i: ?m.3013
i, π: ι → Type ?u.2975
π i: ?m.3013
i) :=
  ⟨fun a: ?m.3083
a => by
Goals accomplished! 🐙
     α: Type ?u.2965

β: Type ?u.2968

ι: Type u

π: ι → Type ?u.2975

inst✝²: Nonempty ι

inst✝¹: (i : ι) → Preorder (π i)

inst✝: ∀ (i : ι), NoMinOrder (π i)

a: (i : ι) → π i

∃ b, b < aclassical
      α: Type ?u.2965

β: Type ?u.2968

ι: Type u

π: ι → Type ?u.2975

inst✝²: Nonempty ι

inst✝¹: (i : ι) → Preorder (π i)

inst✝: ∀ (i : ι), NoMinOrder (π i)

a: (i : ι) → π i

∃ b, b < aobtain ⟨b, hb⟩: ∃ b, b < a (Classical.arbitrary ι)
⟨b: π (Classical.arbitrary ι)
b⟨b, hb⟩: ∃ b, b < a (Classical.arbitrary ι)
, hb: b < a (Classical.arbitrary ι)
hb⟨b, hb⟩: ∃ b, b < a (Classical.arbitrary ι)
⟩ := exists_lt: ∀ {α : Type ?u.3134} [inst : LT α] [self : NoMinOrder α] (a : α), ∃ b, b < a
exists_lt (a: (i : ι) → π i
a <| Classical.arbitrary: (α : Sort ?u.3138) → [h : Nonempty α] → α
Classical.arbitrary _: Sort ?u.3138
_)α: Type ?u.2965

β: Type ?u.2968

ι: Type u

π: ι → Type ?u.2975

inst✝²: Nonempty ι

inst✝¹: (i : ι) → Preorder (π i)

inst✝: ∀ (i : ι), NoMinOrder (π i)

a: (i : ι) → π i

b: π (Classical.arbitrary ι)

hb: b < a (Classical.arbitrary ι)

intro∃ b, b < a
      α: Type ?u.2965

β: Type ?u.2968

ι: Type u

π: ι → Type ?u.2975

inst✝²: Nonempty ι

inst✝¹: (i : ι) → Preorder (π i)

inst✝: ∀ (i : ι), NoMinOrder (π i)

a: (i : ι) → π i

∃ b, b < aexact ⟨_: ?m.3240
_, update_lt_self_iff: ∀ {ι : Type ?u.3249} {π : ι → Type ?u.3250} [inst : DecidableEq ι] [inst_1 : (i : ι) → Preorder (π i)]
  {x : (i : ι) → π i} {i : ι} {a : π i}, Function.update x i a < x ↔ a < x i
update_lt_self_iff.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 hb: b < a (Classical.arbitrary ι)
hb⟩
Goals accomplished! 🐙⟩

-- Porting note: mathlib3 proof uses `convert`
theorem NoBotOrder.to_noMinOrder: ∀ (α : Type u_1) [inst : LinearOrder α] [inst_1 : NoBotOrder α], NoMinOrder α
NoBotOrder.to_noMinOrder (α: Type u_1
α : Type _: Type (?u.3488+1)
Type _) [LinearOrder: Type ?u.3491 → Type ?u.3491
LinearOrder α: Type ?u.3488
α] [NoBotOrder: (α : Type ?u.3494) → [inst : LE α] → Prop
NoBotOrder α: Type ?u.3488
α] : NoMinOrder: (α : Type ?u.3517) → [inst : LT α] → Prop
NoMinOrder α: Type ?u.3488
α :=
  { exists_lt := fun a: ?m.3559
a => by
Goals accomplished! 🐙 α✝: Type ?u.3482

β: Type ?u.3485

α: Type u_1

inst✝¹: LinearOrder α

inst✝: NoBotOrder α

a: α

∃ b, b < asimpa [not_le: ∀ {α : Type ?u.3569} [inst : LinearOrder α] {a b : α}, ¬a ≤ b ↔ b < a
not_le] using exists_not_ge: ∀ {α : Type ?u.4012} [inst : LE α] [self : NoBotOrder α] (a : α), ∃ b, ¬a ≤ b
exists_not_ge a: α
a
Goals accomplished! 🐙 }
#align no_bot_order.to_no_min_order NoBotOrder.to_noMinOrder: ∀ (α : Type u_1) [inst : LinearOrder α] [inst_1 : NoBotOrder α], NoMinOrder α
NoBotOrder.to_noMinOrder

-- Porting note: mathlib3 proof uses `convert`
theorem NoTopOrder.to_noMaxOrder: ∀ (α : Type u_1) [inst : LinearOrder α] [inst_1 : NoTopOrder α], NoMaxOrder α
NoTopOrder.to_noMaxOrder (α: Type ?u.5034
α : Type _: Type (?u.5034+1)
Type _) [LinearOrder: Type ?u.5037 → Type ?u.5037
LinearOrder α: Type ?u.5034
α] [NoTopOrder: (α : Type ?u.5040) → [inst : LE α] → Prop
NoTopOrder α: Type ?u.5034
α] : NoMaxOrder: (α : Type ?u.5063) → [inst : LT α] → Prop
NoMaxOrder α: Type ?u.5034
α :=
  { exists_gt := fun a: ?m.5105
a => by
Goals accomplished! 🐙 α✝: Type ?u.5028

β: Type ?u.5031

α: Type u_1

inst✝¹: LinearOrder α

inst✝: NoTopOrder α

a: α

∃ b, a < bsimpa [not_le: ∀ {α : Type ?u.5115} [inst : LinearOrder α] {a b : α}, ¬a ≤ b ↔ b < a
not_le] using exists_not_le: ∀ {α : Type ?u.5246} [inst : LE α] [self : NoTopOrder α] (a : α), ∃ b, ¬b ≤ a
exists_not_le a: α
a
Goals accomplished! 🐙 }
#align no_top_order.to_no_max_order NoTopOrder.to_noMaxOrder: ∀ (α : Type u_1) [inst : LinearOrder α] [inst_1 : NoTopOrder α], NoMaxOrder α
NoTopOrder.to_noMaxOrder

theorem noBotOrder_iff_noMinOrder: ∀ (α : Type u_1) [inst : LinearOrder α], NoBotOrder α ↔ NoMinOrder α
noBotOrder_iff_noMinOrder (α: Type ?u.5559
α : Type _: Type (?u.5559+1)
Type _) [LinearOrder: Type ?u.5562 → Type ?u.5562
LinearOrder α: Type ?u.5559
α] : NoBotOrder: (α : Type ?u.5565) → [inst : LE α] → Prop
NoBotOrder α: Type ?u.5559
α ↔ NoMinOrder: (α : Type ?u.5586) → [inst : LT α] → Prop
NoMinOrder α: Type ?u.5559
α :=
  ⟨fun h: ?m.5612
h =>
    haveI := h: ?m.5612
h
    NoBotOrder.to_noMinOrder: ∀ (α : Type ?u.5617) [inst : LinearOrder α] [inst_1 : NoBotOrder α], NoMinOrder α
NoBotOrder.to_noMinOrder α: Type u_1
α,
    fun h: ?m.5631
h =>
    haveI := h: ?m.5631
h
    inferInstance: ∀ {α : Sort ?u.5636} [i : α], α
inferInstance⟩
#align no_bot_order_iff_no_min_order noBotOrder_iff_noMinOrder: ∀ (α : Type u_1) [inst : LinearOrder α], NoBotOrder α ↔ NoMinOrder α
noBotOrder_iff_noMinOrder

theorem noTopOrder_iff_noMaxOrder: ∀ (α : Type u_1) [inst : LinearOrder α], NoTopOrder α ↔ NoMaxOrder α
noTopOrder_iff_noMaxOrder (α: Type u_1
α : Type _: Type (?u.5672+1)
Type _) [LinearOrder: Type ?u.5675 → Type ?u.5675
LinearOrder α: Type ?u.5672
α] : NoTopOrder: (α : Type ?u.5678) → [inst : LE α] → Prop
NoTopOrder α: Type ?u.5672
α ↔ NoMaxOrder: (α : Type ?u.5699) → [inst : LT α] → Prop
NoMaxOrder α: Type ?u.5672
α :=
  ⟨fun h: ?m.5725
h =>
    haveI := h: ?m.5725
h
    NoTopOrder.to_noMaxOrder: ∀ (α : Type ?u.5730) [inst : LinearOrder α] [inst_1 : NoTopOrder α], NoMaxOrder α
NoTopOrder.to_noMaxOrder α: Type u_1
α,
    fun h: ?m.5744
h =>
    haveI := h: ?m.5744
h
    inferInstance: ∀ {α : Sort ?u.5749} [i : α], α
inferInstance⟩
#align no_top_order_iff_no_max_order noTopOrder_iff_noMaxOrder: ∀ (α : Type u_1) [inst : LinearOrder α], NoTopOrder α ↔ NoMaxOrder α
noTopOrder_iff_noMaxOrder

theorem NoMinOrder.not_acc: ∀ [inst : LT α] [inst_1 : NoMinOrder α] (a : α), ¬Acc (fun x x_1 => x < x_1) a
NoMinOrder.not_acc [LT: Type ?u.5785 → Type ?u.5785
LT α: Type ?u.5779
α] [NoMinOrder: (α : Type ?u.5788) → [inst : LT α] → Prop
NoMinOrder α: Type ?u.5779
α] (a: α
a : α: Type ?u.5779
α) : ¬Acc: {α : Sort ?u.5798} → (α → α → Prop) → α → Prop
Acc (· < ·): α → α → Prop
(· < ·) a: α
a := fun h: ?m.5848
h =>
  Acc.recOn: ∀ {α : Sort ?u.5850} {r : α → α → Prop} {motive : (a : α) → Acc r a → Sort ?u.5851} {a : α} (t : Acc r a),
  (∀ (x : α) (h : ∀ (y : α), r y x → Acc r y),
      (∀ (y : α) (a : r y x), motive y (_ : Acc r y)) → motive x (_ : Acc r x)) →
    motive a t
Acc.recOn h: ?m.5848
h fun x: ?m.5904
x _: ?m.5907
_ => (exists_lt: ∀ {α : Type ?u.5911} [inst : LT α] [self : NoMinOrder α] (a : α), ∃ b, b < a
exists_lt x: ?m.5904
x).recOn: ∀ {α : Sort ?u.5921} {p : α → Prop} {motive : Exists p → Prop} (t : Exists p),
  (∀ (w : α) (h : p w), motive (_ : Exists p)) → motive t
recOn
#align no_min_order.not_acc NoMinOrder.not_acc: ∀ {α : Type u_1} [inst : LT α] [inst_1 : NoMinOrder α] (a : α), ¬Acc (fun x x_1 => x < x_1) a
NoMinOrder.not_acc

theorem NoMaxOrder.not_acc: ∀ {α : Type u_1} [inst : LT α] [inst_1 : NoMaxOrder α] (a : α), ¬Acc (fun x x_1 => x > x_1) a
NoMaxOrder.not_acc [LT: Type ?u.5986 → Type ?u.5986
LT α: Type ?u.5980
α] [NoMaxOrder: (α : Type ?u.5989) → [inst : LT α] → Prop
NoMaxOrder α: Type ?u.5980
α] (a: α
a : α: Type ?u.5980
α) : ¬Acc: {α : Sort ?u.5999} → (α → α → Prop) → α → Prop
Acc (· > ·): α → α → Prop
(· > ·) a: α
a := fun h: ?m.6049
h =>
  Acc.recOn: ∀ {α : Sort ?u.6051} {r : α → α → Prop} {motive : (a : α) → Acc r a → Sort ?u.6052} {a : α} (t : Acc r a),
  (∀ (x : α) (h : ∀ (y : α), r y x → Acc r y),
      (∀ (y : α) (a : r y x), motive y (_ : Acc r y)) → motive x (_ : Acc r x)) →
    motive a t
Acc.recOn h: ?m.6049
h fun x: ?m.6105
x _: ?m.6108
_ => (exists_gt: ∀ {α : Type ?u.6112} [inst : LT α] [self : NoMaxOrder α] (a : α), ∃ b, a < b
exists_gt x: ?m.6105
x).recOn: ∀ {α : Sort ?u.6122} {p : α → Prop} {motive : Exists p → Prop} (t : Exists p),
  (∀ (w : α) (h : p w), motive (_ : Exists p)) → motive t
recOn
#align no_max_order.not_acc NoMaxOrder.not_acc: ∀ {α : Type u_1} [inst : LT α] [inst_1 : NoMaxOrder α] (a : α), ¬Acc (fun x x_1 => x > x_1) a
NoMaxOrder.not_acc

section LE

variable [LE: Type ?u.7002 → Type ?u.7002
LE α: Type ?u.6996
α] {a: α
a b: α
b : α: Type ?u.6189
α}

/-- `a : α` is a bottom element of `α` if it is less than or equal to any other element of `α`.
This predicate is roughly an unbundled version of `OrderBot`, except that a preorder may have
several bottom elements. When `α` is linear, this is useful to make a case disjunction on
`NoMinOrder α` within a proof. -/
def IsBot: {α : Type u_1} → [inst : LE α] → α → Prop
IsBot (a: α
a : α: Type ?u.6202
α) : Prop: Type
Prop :=
  ∀ b: ?m.6220
b, a: α
a ≤ b: ?m.6220
b
#align is_bot IsBot: {α : Type u_1} → [inst : LE α] → α → Prop
IsBot

/-- `a : α` is a top element of `α` if it is greater than or equal to any other element of `α`.
This predicate is roughly an unbundled version of `OrderBot`, except that a preorder may have
several top elements. When `α` is linear, this is useful to make a case disjunction on
`NoMaxOrder α` within a proof. -/
def IsTop: α → Prop
IsTop (a: α
a : α: Type ?u.6240
α) : Prop: Type
Prop :=
  ∀ b: ?m.6258
b, b: ?m.6258
b ≤ a: α
a
#align is_top IsTop: {α : Type u_1} → [inst : LE α] → α → Prop
IsTop

/-- `a` is a minimal element of `α` if no element is strictly less than it. We spell it without `<`
to avoid having to convert between `≤` and `<`. Instead, `isMin_iff_forall_not_lt` does the
conversion. -/
def IsMin: α → Prop
IsMin (a: α
a : α: Type ?u.6278
α) : Prop: Type
Prop :=
  ∀ ⦃b: ?m.6296
b⦄, b: ?m.6296
b ≤ a: α
a → a: α
a ≤ b: ?m.6296
b
#align is_min IsMin: {α : Type u_1} → [inst : LE α] → α → Prop
IsMin

/-- `a` is a maximal element of `α` if no element is strictly greater than it. We spell it without
`<` to avoid having to convert between `≤` and `<`. Instead, `isMax_iff_forall_not_lt` does the
conversion. -/
def IsMax: {α : Type u_1} → [inst : LE α] → α → Prop
IsMax (a: α
a : α: Type ?u.6324
α) : Prop: Type
Prop :=
  ∀ ⦃b: ?m.6342
b⦄, a: α
a ≤ b: ?m.6342
b → b: ?m.6342
b ≤ a: α
a
#align is_max IsMax: {α : Type u_1} → [inst : LE α] → α → Prop
IsMax

@[simp]
theorem not_isBot: ∀ [inst : NoBotOrder α] (a : α), ¬IsBot a
not_isBot [NoBotOrder: (α : Type ?u.6383) → [inst : LE α] → Prop
NoBotOrder α: Type ?u.6370
α] (a: α
a : α: Type ?u.6370
α) : ¬IsBot: {α : Type ?u.6393} → [inst : LE α] → α → Prop
IsBot a: α
a := fun h: ?m.6404
h =>
  let ⟨_, hb: ¬a ≤ w✝
hb⟩ := exists_not_ge: ∀ {α : Type ?u.6406} [inst : LE α] [self : NoBotOrder α] (a : α), ∃ b, ¬a ≤ b
exists_not_ge a: α
a
  hb: ¬a ≤ w✝
hb <| h: ?m.6404
h _: α
_
#align not_is_bot not_isBot: ∀ {α : Type u_1} [inst : LE α] [inst_1 : NoBotOrder α] (a : α), ¬IsBot a
not_isBot

@[simp]
theorem not_isTop: ∀ {α : Type u_1} [inst : LE α] [inst_1 : NoTopOrder α] (a : α), ¬IsTop a
not_isTop [NoTopOrder: (α : Type ?u.6562) → [inst : LE α] → Prop
NoTopOrder α: Type ?u.6549
α] (a: α
a : α: Type ?u.6549
α) : ¬IsTop: {α : Type ?u.6572} → [inst : LE α] → α → Prop
IsTop a: α
a := fun h: ?m.6583
h =>
  let ⟨_, hb: ¬w✝ ≤ a
hb⟩ := exists_not_le: ∀ {α : Type ?u.6585} [inst : LE α] [self : NoTopOrder α] (a : α), ∃ b, ¬b ≤ a
exists_not_le a: α
a
  hb: ¬w✝ ≤ a
hb <| h: ?m.6583
h _: α
_
#align not_is_top not_isTop: ∀ {α : Type u_1} [inst : LE α] [inst_1 : NoTopOrder α] (a : α), ¬IsTop a
not_isTop

protected theorem IsBot.isMin: IsBot a → IsMin a
IsBot.isMin (h: IsBot a
h : IsBot: {α : Type ?u.6741} → [inst : LE α] → α → Prop
IsBot a: α
a) : IsMin: {α : Type ?u.6761} → [inst : LE α] → α → Prop
IsMin a: α
a := fun b: ?m.6779
b _: ?m.6782
_ => h: IsBot a
h b: ?m.6779
b
#align is_bot.is_min IsBot.isMin: ∀ {α : Type u_1} [inst : LE α] {a : α}, IsBot a → IsMin a
IsBot.isMin

protected theorem IsTop.isMax: ∀ {α : Type u_1} [inst : LE α] {a : α}, IsTop a → IsMax a
IsTop.isMax (h: IsTop a
h : IsTop: {α : Type ?u.6806} → [inst : LE α] → α → Prop
IsTop a: α
a) : IsMax: {α : Type ?u.6826} → [inst : LE α] → α → Prop
IsMax a: α
a := fun b: ?m.6844
b _: ?m.6847
_ => h: IsTop a
h b: ?m.6844
b
#align is_top.is_max IsTop.isMax: ∀ {α : Type u_1} [inst : LE α] {a : α}, IsTop a → IsMax a
IsTop.isMax

@[simp]
theorem isBot_toDual_iff: IsBot (↑toDual a) ↔ IsTop a
isBot_toDual_iff : IsBot: {α : Type ?u.6871} → [inst : LE α] → α → Prop
IsBot (toDual: {α : Type ?u.6874} → α ≃ αᵒᵈ
toDual a: α
a) ↔ IsTop: {α : Type ?u.6949} → [inst : LE α] → α → Prop
IsTop a: α
a :=
  Iff.rfl: ∀ {a : Prop}, a ↔ a
Iff.rfl
#align is_bot_to_dual_iff isBot_toDual_iff: ∀ {α : Type u_1} [inst : LE α] {a : α}, IsBot (↑toDual a) ↔ IsTop a
isBot_toDual_iff

@[simp]
theorem isTop_toDual_iff: ∀ {α : Type u_1} [inst : LE α] {a : α}, IsTop (↑toDual a) ↔ IsBot a
isTop_toDual_iff : IsTop: {α : Type ?u.7009} → [inst : LE α] → α → Prop
IsTop (toDual: {α : Type ?u.7012} → α ≃ αᵒᵈ
toDual a: α
a) ↔ IsBot: {α : Type ?u.7087} → [inst : LE α] → α → Prop
IsBot a: α
a :=
  Iff.rfl: ∀ {a : Prop}, a ↔ a
Iff.rfl
#align is_top_to_dual_iff isTop_toDual_iff: ∀ {α : Type u_1} [inst : LE α] {a : α}, IsTop (↑toDual a) ↔ IsBot a
isTop_toDual_iff

@[simp]
theorem isMin_toDual_iff: IsMin (↑toDual a) ↔ IsMax a
isMin_toDual_iff : IsMin: {α : Type ?u.7147} → [inst : LE α] → α → Prop
IsMin (toDual: {α : Type ?u.7150} → α ≃ αᵒᵈ
toDual a: α
a) ↔ IsMax: {α : Type ?u.7225} → [inst : LE α] → α → Prop
IsMax a: α
a :=
  Iff.rfl: ∀ {a : Prop}, a ↔ a
Iff.rfl
#align is_min_to_dual_iff isMin_toDual_iff: ∀ {α : Type u_1} [inst : LE α] {a : α}, IsMin (↑toDual a) ↔ IsMax a
isMin_toDual_iff

@[simp]
theorem isMax_toDual_iff: ∀ {α : Type u_1} [inst : LE α] {a : α}, IsMax (↑toDual a) ↔ IsMin a
isMax_toDual_iff : IsMax: {α : Type ?u.7287} → [inst : LE α] → α → Prop
IsMax (toDual: {α : Type ?u.7290} → α ≃ αᵒᵈ
toDual a: α
a) ↔ IsMin: {α : Type ?u.7365} → [inst : LE α] → α → Prop
IsMin a: α
a :=
  Iff.rfl: ∀ {a : Prop}, a ↔ a
Iff.rfl
#align is_max_to_dual_iff isMax_toDual_iff: ∀ {α : Type u_1} [inst : LE α] {a : α}, IsMax (↑toDual a) ↔ IsMin a
isMax_toDual_iff

@[simp]
theorem isBot_ofDual_iff: ∀ {α : Type u_1} [inst : LE α] {a : αᵒᵈ}, IsBot (↑ofDual a) ↔ IsTop a
isBot_ofDual_iff {a: αᵒᵈ
a : α: Type ?u.7414
αᵒᵈ} : IsBot: {α : Type ?u.7430} → [inst : LE α] → α → Prop
IsBot (ofDual: {α : Type ?u.7433} → αᵒᵈ ≃ α
ofDual a: αᵒᵈ
a) ↔ IsTop: {α : Type ?u.7503} → [inst : LE α] → α → Prop
IsTop a: αᵒᵈ
a :=
  Iff.rfl: ∀ {a : Prop}, a ↔ a
Iff.rfl
#align is_bot_of_dual_iff isBot_ofDual_iff: ∀ {α : Type u_1} [inst : LE α] {a : αᵒᵈ}, IsBot (↑ofDual a) ↔ IsTop a
isBot_ofDual_iff

@[simp]
theorem isTop_ofDual_iff: ∀ {α : Type u_1} [inst : LE α] {a : αᵒᵈ}, IsTop (↑ofDual a) ↔ IsBot a
isTop_ofDual_iff {a: αᵒᵈ
a : α: Type ?u.7557
αᵒᵈ} : IsTop: {α : Type ?u.7573} → [inst : LE α] → α → Prop
IsTop (ofDual: {α : Type ?u.7576} → αᵒᵈ ≃ α
ofDual a: αᵒᵈ
a) ↔ IsBot: {α : Type ?u.7646} → [inst : LE α] → α → Prop
IsBot a: αᵒᵈ
a :=
  Iff.rfl: ∀ {a : Prop}, a ↔ a
Iff.rfl
#align is_top_of_dual_iff isTop_ofDual_iff: ∀ {α : Type u_1} [inst : LE α] {a : αᵒᵈ}, IsTop (↑ofDual a) ↔ IsBot a
isTop_ofDual_iff

@[simp]
theorem isMin_ofDual_iff: ∀ {α : Type u_1} [inst : LE α] {a : αᵒᵈ}, IsMin (↑ofDual a) ↔ IsMax a
isMin_ofDual_iff {a: αᵒᵈ
a : α: Type ?u.7700
αᵒᵈ} : IsMin: {α : Type ?u.7716} → [inst : LE α] → α → Prop
IsMin (ofDual: {α : Type ?u.7719} → αᵒᵈ ≃ α
ofDual a: αᵒᵈ
a) ↔ IsMax: {α : Type ?u.7789} → [inst : LE α] → α → Prop
IsMax a: αᵒᵈ
a :=
  Iff.rfl: ∀ {a : Prop}, a ↔ a
Iff.rfl
#align is_min_of_dual_iff isMin_ofDual_iff: ∀ {α : Type u_1} [inst : LE α] {a : αᵒᵈ}, IsMin (↑ofDual a) ↔ IsMax a
isMin_ofDual_iff

@[simp]
theorem isMax_ofDual_iff: ∀ {α : Type u_1} [inst : LE α] {a : αᵒᵈ}, IsMax (↑ofDual a) ↔ IsMin a
isMax_ofDual_iff {a: αᵒᵈ
a : α: Type ?u.7845
αᵒᵈ} : IsMax: {α : Type ?u.7861} → [inst : LE α] → α → Prop
IsMax (ofDual: {α : Type ?u.7864} → αᵒᵈ ≃ α
ofDual a: αᵒᵈ
a) ↔ IsMin: {α : Type ?u.7934} → [inst : LE α] → α → Prop
IsMin a: αᵒᵈ
a :=
  Iff.rfl: ∀ {a : Prop}, a ↔ a
Iff.rfl
#align is_max_of_dual_iff isMax_ofDual_iff: ∀ {α : Type u_1} [inst : LE α] {a : αᵒᵈ}, IsMax (↑ofDual a) ↔ IsMin a
isMax_ofDual_iff

alias isBot_toDual_iff: ∀ {α : Type u_1} [inst : LE α] {a : α}, IsBot (↑toDual a) ↔ IsTop a
isBot_toDual_iff ↔ _ IsTop.toDual: ∀ {α : Type u_1} [inst : LE α] {a : α}, IsTop a → IsBot (↑toDual a)
IsTop.toDual
#align is_top.to_dual IsTop.toDual: ∀ {α : Type u_1} [inst : LE α] {a : α}, IsTop a → IsBot (↑toDual a)
IsTop.toDual

alias isTop_toDual_iff: ∀ {α : Type u_1} [inst : LE α] {a : α}, IsTop (↑toDual a) ↔ IsBot a
isTop_toDual_iff ↔ _ IsBot.toDual: ∀ {α : Type u_1} [inst : LE α] {a : α}, IsBot a → IsTop (↑toDual a)
IsBot.toDual
#align is_bot.to_dual IsBot.toDual: ∀ {α : Type u_1} [inst : LE α] {a : α}, IsBot a → IsTop (↑toDual a)
IsBot.toDual

alias isMin_toDual_iff: ∀ {α : Type u_1} [inst : LE α] {a : α}, IsMin (↑toDual a) ↔ IsMax a
isMin_toDual_iff ↔ _ IsMax.toDual: ∀ {α : Type u_1} [inst : LE α] {a : α}, IsMax a → IsMin (↑toDual a)
IsMax.toDual
#align is_max.to_dual IsMax.toDual: ∀ {α : Type u_1} [inst : LE α] {a : α}, IsMax a → IsMin (↑toDual a)
IsMax.toDual

alias isMax_toDual_iff: ∀ {α : Type u_1} [inst : LE α] {a : α}, IsMax (↑toDual a) ↔ IsMin a
isMax_toDual_iff ↔ _ IsMin.toDual: ∀ {α : Type u_1} [inst : LE α] {a : α}, IsMin a → IsMax (↑toDual a)
IsMin.toDual
#align is_min.to_dual IsMin.toDual: ∀ {α : Type u_1} [inst : LE α] {a : α}, IsMin a → IsMax (↑toDual a)
IsMin.toDual

alias isBot_ofDual_iff: ∀ {α : Type u_1} [inst : LE α] {a : αᵒᵈ}, IsBot (↑ofDual a) ↔ IsTop a
isBot_ofDual_iff ↔ _ IsTop.ofDual: ∀ {α : Type u_1} [inst : LE α] {a : αᵒᵈ}, IsTop a → IsBot (↑ofDual a)
IsTop.ofDual
#align is_top.of_dual IsTop.ofDual: ∀ {α : Type u_1} [inst : LE α] {a : αᵒᵈ}, IsTop a → IsBot (↑ofDual a)
IsTop.ofDual

alias isTop_ofDual_iff: ∀ {α : Type u_1} [inst : LE α] {a : αᵒᵈ}, IsTop (↑ofDual a) ↔ IsBot a
isTop_ofDual_iff ↔ _ IsBot.ofDual: ∀ {α : Type u_1} [inst : LE α] {a : αᵒᵈ}, IsBot a → IsTop (↑ofDual a)
IsBot.ofDual
#align is_bot.of_dual IsBot.ofDual: ∀ {α : Type u_1} [inst : LE α] {a : αᵒᵈ}, IsBot a → IsTop (↑ofDual a)
IsBot.ofDual

alias isMin_ofDual_iff: ∀ {α : Type u_1} [inst : LE α] {a : αᵒᵈ}, IsMin (↑ofDual a) ↔ IsMax a
isMin_ofDual_iff ↔ _ IsMax.ofDual: ∀ {α : Type u_1} [inst : LE α] {a : αᵒᵈ}, IsMax a → IsMin (↑ofDual a)
IsMax.ofDual
#align is_max.of_dual IsMax.ofDual: ∀ {α : Type u_1} [inst : LE α] {a : αᵒᵈ}, IsMax a → IsMin (↑ofDual a)
IsMax.ofDual

alias isMax_ofDual_iff: ∀ {α : Type u_1} [inst : LE α] {a : αᵒᵈ}, IsMax (↑ofDual a) ↔ IsMin a
isMax_ofDual_iff ↔ _ IsMin.ofDual: ∀ {α : Type u_1} [inst : LE α] {a : αᵒᵈ}, IsMin a → IsMax (↑ofDual a)
IsMin.ofDual
#align is_min.of_dual IsMin.ofDual: ∀ {α : Type u_1} [inst : LE α] {a : αᵒᵈ}, IsMin a → IsMax (↑ofDual a)
IsMin.ofDual

end LE

section Preorder

variable [Preorder: Type ?u.8057 → Type ?u.8057
Preorder α: Type ?u.8867
α] {a: α
a b: α
b : α: Type ?u.8773
α}

theorem IsBot.mono: IsBot a → b ≤ a → IsBot b
IsBot.mono (ha: IsBot a
ha : IsBot: {α : Type ?u.8064} → [inst : LE α] → α → Prop
IsBot a: α
a) (h: b ≤ a
h : b: α
b ≤ a: α
a) : IsBot: {α : Type ?u.8096} → [inst : LE α] → α → Prop
IsBot b: α
b := fun _: ?m.8117
_ => h: b ≤ a
h.trans: ∀ {α : Type ?u.8119} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ c
trans <| ha: IsBot a
ha _: α
_
#align is_bot.mono IsBot.mono: ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, IsBot a → b ≤ a → IsBot b
IsBot.mono

theorem IsTop.mono: IsTop a → a ≤ b → IsTop b
IsTop.mono (ha: IsTop a
ha : IsTop: {α : Type ?u.8163} → [inst : LE α] → α → Prop
IsTop a: α
a) (h: a ≤ b
h : a: α
a ≤ b: α
b) : IsTop: {α : Type ?u.8195} → [inst : LE α] → α → Prop
IsTop b: α
b := fun _: ?m.8216
_ => (ha: IsTop a
ha _: α
_).trans: ∀ {α : Type ?u.8219} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ c
trans h: a ≤ b
h
#align is_top.mono IsTop.mono: ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, IsTop a → a ≤ b → IsTop b
IsTop.mono

theorem IsMin.mono: ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, IsMin a → b ≤ a → IsMin b
IsMin.mono (ha: IsMin a
ha : IsMin: {α : Type ?u.8262} → [inst : LE α] → α → Prop
IsMin a: α
a) (h: b ≤ a
h : b: α
b ≤ a: α
a) : IsMin: {α : Type ?u.8294} → [inst : LE α] → α → Prop
IsMin b: α
b := fun _: ?m.8315
_ hc: ?m.8318
hc => h: b ≤ a
h.trans: ∀ {α : Type ?u.8320} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ c
trans <| ha: IsMin a
ha <| hc: ?m.8318
hc.trans: ∀ {α : Type ?u.8342} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ c
trans h: b ≤ a
h
#align is_min.mono IsMin.mono: ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, IsMin a → b ≤ a → IsMin b
IsMin.mono

theorem IsMax.mono: ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, IsMax a → a ≤ b → IsMax b
IsMax.mono (ha: IsMax a
ha : IsMax: {α : Type ?u.8379} → [inst : LE α] → α → Prop
IsMax a: α
a) (h: a ≤ b
h : a: α
a ≤ b: α
b) : IsMax: {α : Type ?u.8411} → [inst : LE α] → α → Prop
IsMax b: α
b := fun _: ?m.8432
_ hc: ?m.8435
hc => (ha: IsMax a
ha <| h: a ≤ b
h.trans: ∀ {α : Type ?u.8438} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ c
trans hc: ?m.8435
hc).trans: ∀ {α : Type ?u.8459} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ c
trans h: a ≤ b
h
#align is_max.mono IsMax.mono: ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, IsMax a → a ≤ b → IsMax b
IsMax.mono

theorem IsMin.not_lt: ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, IsMin a → ¬b < a
IsMin.not_lt (h: IsMin a
h : IsMin: {α : Type ?u.8496} → [inst : LE α] → α → Prop
IsMin a: α
a) : ¬b: α
b < a: α
a := fun hb: ?m.8537
hb => hb: ?m.8537
hb.not_le: ∀ {α : Type ?u.8539} [inst : Preorder α] {a b : α}, a < b → ¬b ≤ a
not_le <| h: IsMin a
h hb: ?m.8537
hb.le: ∀ {α : Type ?u.8563} [inst : Preorder α] {a b : α}, a < b → a ≤ b
le
#align is_min.not_lt IsMin.not_lt: ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, IsMin a → ¬b < a
IsMin.not_lt

theorem IsMax.not_lt: IsMax a → ¬a < b
IsMax.not_lt (h: IsMax a
h : IsMax: {α : Type ?u.8594} → [inst : LE α] → α → Prop
IsMax a: α
a) : ¬a: α
a < b: α
b := fun hb: ?m.8635
hb => hb: ?m.8635
hb.not_le: ∀ {α : Type ?u.8637} [inst : Preorder α] {a b : α}, a < b → ¬b ≤ a
not_le <| h: IsMax a
h hb: ?m.8635
hb.le: ∀ {α : Type ?u.8661} [inst : Preorder α] {a b : α}, a < b → a ≤ b
le
#align is_max.not_lt IsMax.not_lt: ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, IsMax a → ¬a < b
IsMax.not_lt

@[simp]
theorem not_isMin_of_lt: ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, b < a → ¬IsMin a
not_isMin_of_lt (h: b < a
h : b: α
b < a: α
a) : ¬IsMin: {α : Type ?u.8707} → [inst : LE α] → α → Prop
IsMin a: α
a := fun ha: ?m.8721
ha => ha: ?m.8721
ha.not_lt: ∀ {α : Type ?u.8723} [inst : Preorder α] {a b : α}, IsMin a → ¬b < a
not_lt h: b < a
h
#align not_is_min_of_lt not_isMin_of_lt: ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, b < a → ¬IsMin a
not_isMin_of_lt

@[simp]
theorem not_isMax_of_lt: ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a < b → ¬IsMax a
not_isMax_of_lt (h: a < b
h : a: α
a < b: α
b) : ¬IsMax: {α : Type ?u.8801} → [inst : LE α] → α → Prop
IsMax a: α
a := fun ha: ?m.8815
ha => ha: ?m.8815
ha.not_lt: ∀ {α : Type ?u.8817} [inst : Preorder α] {a b : α}, IsMax a → ¬a < b
not_lt h: a < b
h
#align not_is_max_of_lt not_isMax_of_lt: ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a < b → ¬IsMax a
not_isMax_of_lt

alias not_isMin_of_lt: ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, b < a → ¬IsMin a
not_isMin_of_lt ← LT.lt.not_isMin: ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, b < a → ¬IsMin a
LT.lt.not_isMin

alias not_isMax_of_lt: ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a < b → ¬IsMax a
not_isMax_of_lt ← LT.lt.not_isMax: ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a < b → ¬IsMax a
LT.lt.not_isMax

theorem isMin_iff_forall_not_lt: IsMin a ↔ ∀ (b : α), ¬b < a
isMin_iff_forall_not_lt : IsMin: {α : Type ?u.8880} → [inst : LE α] → α → Prop
IsMin a: α
a ↔ ∀ b: ?m.8894
b, ¬b: ?m.8894
b < a: α
a :=
  ⟨fun h: ?m.8919
h _: ?m.8922
_ => h: ?m.8919
h.not_lt: ∀ {α : Type ?u.8924} [inst : Preorder α] {a b : α}, IsMin a → ¬b < a
not_lt, fun h: ?m.8953
h _: ?m.8957
_ hba: ?m.8960
hba => of_not_not: ∀ {a : Prop}, ¬¬a → a
of_not_not fun hab: ?m.8964
hab => h: ?m.8953
h _: α
_ <| hba: ?m.8960
hba.lt_of_not_le: ∀ {α : Type ?u.8967} [inst : Preorder α] {a b : α}, a ≤ b → ¬b ≤ a → a < b
lt_of_not_le hab: ?m.8964
hab⟩
#align is_min_iff_forall_not_lt isMin_iff_forall_not_lt: ∀ {α : Type u_1} [inst : Preorder α] {a : α}, IsMin a ↔ ∀ (b : α), ¬b < a
isMin_iff_forall_not_lt

theorem isMax_iff_forall_not_lt: ∀ {α : Type u_1} [inst : Preorder α] {a : α}, IsMax a ↔ ∀ (b : α), ¬a < b
isMax_iff_forall_not_lt : IsMax: {α : Type ?u.9015} → [inst : LE α] → α → Prop
IsMax a: α
a ↔ ∀ b: ?m.9029
b, ¬a: α
a < b: ?m.9029
b :=
  ⟨fun h: ?m.9054
h _: ?m.9057
_ => h: ?m.9054
h.not_lt: ∀ {α : Type ?u.9059} [inst : Preorder α] {a b : α}, IsMax a → ¬a < b
not_lt, fun h: ?m.9088
h _: ?m.9092
_ hba: ?m.9095
hba => of_not_not: ∀ {a : Prop}, ¬¬a → a
of_not_not fun hab: ?m.9099
hab => h: ?m.9088
h _: α
_ <| hba: ?m.9095
hba.lt_of_not_le: ∀ {α : Type ?u.9102} [inst : Preorder α] {a b : α}, a ≤ b → ¬b ≤ a → a < b
lt_of_not_le hab: ?m.9099
hab⟩
#align is_max_iff_forall_not_lt isMax_iff_forall_not_lt: ∀ {α : Type u_1} [inst : Preorder α] {a : α}, IsMax a ↔ ∀ (b : α), ¬a < b
isMax_iff_forall_not_lt

@[simp]
theorem not_isMin_iff: ∀ {α : Type u_1} [inst : Preorder α] {a : α}, ¬IsMin a ↔ ∃ b, b < a
not_isMin_iff : ¬IsMin: {α : Type ?u.9150} → [inst : LE α] → α → Prop
IsMin a: α
a ↔ ∃ b: ?m.9166
b, b: ?m.9166
b < a: α
a := by
Goals accomplished! 🐙
  α: Type u_1

β: Type ?u.9140

inst✝: Preorder α

a, b: α

¬IsMin a ↔ ∃ b, b < asimp [lt_iff_le_not_le: ∀ {α : Type ?u.9182} [inst : Preorder α] {a b : α}, a < b ↔ a ≤ b ∧ ¬b ≤ a
lt_iff_le_not_le, IsMin: {α : Type ?u.9204} → [inst : LE α] → α → Prop
IsMin, not_forall: ∀ {α : Sort ?u.9206} {p : α → Prop}, (¬∀ (x : α), p x) ↔ ∃ x, ¬p x
not_forall, exists_prop: ∀ {b a : Prop}, (∃ _h, b) ↔ a ∧ b
exists_prop]
Goals accomplished! 🐙
#align not_is_min_iff not_isMin_iff: ∀ {α : Type u_1} [inst : Preorder α] {a : α}, ¬IsMin a ↔ ∃ b, b < a
not_isMin_iff

@[simp]
theorem not_isMax_iff: ∀ {α : Type u_1} [inst : Preorder α] {a : α}, ¬IsMax a ↔ ∃ b, a < b
not_isMax_iff : ¬IsMax: {α : Type ?u.12559} → [inst : LE α] → α → Prop
IsMax a: α
a ↔ ∃ b: ?m.12575
b, a: α
a < b: ?m.12575
b := by
Goals accomplished! 🐙
  α: Type u_1

β: Type ?u.12549

inst✝: Preorder α

a, b: α

¬IsMax a ↔ ∃ b, a < bsimp [lt_iff_le_not_le: ∀ {α : Type ?u.12591} [inst : Preorder α] {a b : α}, a < b ↔ a ≤ b ∧ ¬b ≤ a
lt_iff_le_not_le, IsMax: {α : Type ?u.12613} → [inst : LE α] → α → Prop
IsMax, not_forall: ∀ {α : Sort ?u.12615} {p : α → Prop}, (¬∀ (x : α), p x) ↔ ∃ x, ¬p x
not_forall, exists_prop: ∀ {b a : Prop}, (∃ _h, b) ↔ a ∧ b
exists_prop]
Goals accomplished! 🐙
#align not_is_max_iff not_isMax_iff: ∀ {α : Type u_1} [inst : Preorder α] {a : α}, ¬IsMax a ↔ ∃ b, a < b
not_isMax_iff

@[simp]
theorem not_isMin: ∀ [inst : NoMinOrder α] (a : α), ¬IsMin a
not_isMin [NoMinOrder: (α : Type ?u.15961) → [inst : LT α] → Prop
NoMinOrder α: Type ?u.15948
α] (a: α
a : α: Type ?u.15948
α) : ¬IsMin: {α : Type ?u.15977} → [inst : LE α] → α → Prop
IsMin a: α
a :=
  not_isMin_iff: ∀ {α : Type ?u.15992} [inst : Preorder α] {a : α}, ¬IsMin a ↔ ∃ b, b < a
not_isMin_iff.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 <| exists_lt: ∀ {α : Type ?u.16018} [inst : LT α] [self : NoMinOrder α] (a : α), ∃ b, b < a
exists_lt a: α
a
#align not_is_min not_isMin: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : NoMinOrder α] (a : α), ¬IsMin a
not_isMin

@[simp]
theorem not_isMax: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : NoMaxOrder α] (a : α), ¬IsMax a
not_isMax [NoMaxOrder: (α : Type ?u.16073) → [inst : LT α] → Prop
NoMaxOrder α: Type ?u.16060
α] (a: α
a : α: Type ?u.16060
α) : ¬IsMax: {α : Type ?u.16089} → [inst : LE α] → α → Prop
IsMax a: α
a :=
  not_isMax_iff: ∀ {α : Type ?u.16104} [inst : Preorder α] {a : α}, ¬IsMax a ↔ ∃ b, a < b
not_isMax_iff.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 <| exists_gt: ∀ {α : Type ?u.16130} [inst : LT α] [self : NoMaxOrder α] (a : α), ∃ b, a < b
exists_gt a: α
a
#align not_is_max not_isMax: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : NoMaxOrder α] (a : α), ¬IsMax a
not_isMax

namespace Subsingleton

variable [Subsingleton: Sort ?u.16201 → Prop
Subsingleton α: Type ?u.16436
α]

protected theorem isBot: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : Subsingleton α] (a : α), IsBot a
isBot (a: α
a : α: Type ?u.16188
α) : IsBot: {α : Type ?u.16206} → [inst : LE α] → α → Prop
IsBot a: α
a := fun _: ?m.16235
_ => (Subsingleton.elim: ∀ {α : Sort ?u.16237} [h : Subsingleton α] (a b : α), a = b
Subsingleton.elim _: ?m.16238
_ _: ?m.16238
_).le: ∀ {α : Type ?u.16264} [inst : Preorder α] {a b : α}, a = b → a ≤ b
le
#align subsingleton.is_bot Subsingleton.isBot: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : Subsingleton α] (a : α), IsBot a
Subsingleton.isBot

protected theorem isTop: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : Subsingleton α] (a : α), IsTop a
isTop (a: α
a : α: Type ?u.16312
α) : IsTop: {α : Type ?u.16330} → [inst : LE α] → α → Prop
IsTop a: α
a := fun _: ?m.16359
_ => (Subsingleton.elim: ∀ {α : Sort ?u.16361} [h : Subsingleton α] (a b : α), a = b
Subsingleton.elim _: ?m.16362
_ _: ?m.16362
_).le: ∀ {α : Type ?u.16388} [inst : Preorder α] {a b : α}, a = b → a ≤ b
le
#align subsingleton.is_top Subsingleton.isTop: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : Subsingleton α] (a : α), IsTop a
Subsingleton.isTop

protected theorem isMin: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : Subsingleton α] (a : α), IsMin a
isMin (a: α
a : α: Type ?u.16436
α) : IsMin: {α : Type ?u.16454} → [inst : LE α] → α → Prop
IsMin a: α
a :=
  (Subsingleton.isBot: ∀ {α : Type ?u.16482} [inst : Preorder α] [inst_1 : Subsingleton α] (a : α), IsBot a
Subsingleton.isBot _: ?m.16483
_).isMin: ∀ {α : Type ?u.16519} [inst : LE α] {a : α}, IsBot a → IsMin a
isMin
#align subsingleton.is_min Subsingleton.isMin: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : Subsingleton α] (a : α), IsMin a
Subsingleton.isMin

protected theorem isMax: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : Subsingleton α] (a : α), IsMax a
isMax (a: α
a : α: Type ?u.16571
α) : IsMax: {α : Type ?u.16589} → [inst : LE α] → α → Prop
IsMax a: α
a :=
  (Subsingleton.isTop: ∀ {α : Type ?u.16617} [inst : Preorder α] [inst_1 : Subsingleton α] (a : α), IsTop a
Subsingleton.isTop _: ?m.16618
_).isMax: ∀ {α : Type ?u.16654} [inst : LE α] {a : α}, IsTop a → IsMax a
isMax
#align subsingleton.is_max Subsingleton.isMax: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : Subsingleton α] (a : α), IsMax a
Subsingleton.isMax

end Subsingleton

end Preorder

section PartialOrder

variable [PartialOrder: Type ?u.16712 → Type ?u.16712
PartialOrder α: Type ?u.16804
α] {a: α
a b: α
b : α: Type ?u.16706
α}

protected theorem IsMin.eq_of_le: ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, IsMin a → b ≤ a → b = a
IsMin.eq_of_le (ha: IsMin a
ha : IsMin: {α : Type ?u.16732} → [inst : LE α] → α → Prop
IsMin a: α
a) (h: b ≤ a
h : b: α
b ≤ a: α
a) : b: α
b = a: α
a :=
  h: b ≤ a
h.antisymm: ∀ {α : Type ?u.16774} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → a = b
antisymm <| ha: IsMin a
ha h: b ≤ a
h
#align is_min.eq_of_le IsMin.eq_of_le: ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, IsMin a → b ≤ a → b = a
IsMin.eq_of_le

protected theorem IsMin.eq_of_ge: IsMin a → b ≤ a → a = b
IsMin.eq_of_ge (ha: IsMin a
ha : IsMin: {α : Type ?u.16817} → [inst : LE α] → α → Prop
IsMin a: α
a) (h: b ≤ a
h : b: α
b ≤ a: α
a) : a: α
a = b: α
b :=
  h: b ≤ a
h.antisymm': ∀ {α : Type ?u.16859} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → b = a
antisymm' <| ha: IsMin a
ha h: b ≤ a
h
#align is_min.eq_of_ge IsMin.eq_of_ge: ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, IsMin a → b ≤ a → a = b
IsMin.eq_of_ge

protected theorem IsMax.eq_of_le: IsMax a → a ≤ b → a = b
IsMax.eq_of_le (ha: IsMax a
ha : IsMax: {α : Type ?u.16902} → [inst : LE α] → α → Prop
IsMax a: α
a) (h: a ≤ b
h : a: α
a ≤ b: α
b) : a: α
a = b: α
b :=
  h: a ≤ b
h.antisymm: ∀ {α : Type ?u.16944} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → a = b
antisymm <| ha: IsMax a
ha h: a ≤ b
h
#align is_max.eq_of_le IsMax.eq_of_le: ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, IsMax a → a ≤ b → a = b
IsMax.eq_of_le

protected theorem IsMax.eq_of_ge: ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, IsMax a → a ≤ b → b = a
IsMax.eq_of_ge (ha: IsMax a
ha : IsMax: {α : Type ?u.16987} → [inst : LE α] → α → Prop
IsMax a: α
a) (h: a ≤ b
h : a: α
a ≤ b: α
b) : b: α
b = a: α
a :=
  h: a ≤ b
h.antisymm': ∀ {α : Type ?u.17029} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → b = a
antisymm' <| ha: IsMax a
ha h: a ≤ b
h
#align is_max.eq_of_ge IsMax.eq_of_ge: ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, IsMax a → a ≤ b → b = a
IsMax.eq_of_ge

end PartialOrder

section Prod

variable [Preorder: Type ?u.18204 → Type ?u.18204
Preorder α: Type ?u.17260
α] [Preorder: Type ?u.17438 → Type ?u.17438
Preorder β: Type ?u.17094
β] {a: α
a a₁: α
a₁ a₂: α
a₂ : α: Type ?u.19443
α} {b: β
b b₁: β
b₁ b₂: β
b₂ : β: Type ?u.17062
β} {x: α × β
x y: α × β
y : α: Type ?u.17059
α × β: Type ?u.17062
β}

theorem IsBot.prod_mk: ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {a : α} {b : β},
  IsBot a → IsBot b → IsBot (a, b)
IsBot.prod_mk (ha: IsBot a
ha : IsBot: {α : Type ?u.17123} → [inst : LE α] → α → Prop
IsBot a: α
a) (hb: IsBot b
hb : IsBot: {α : Type ?u.17150} → [inst : LE α] → α → Prop
IsBot b: β
b) : IsBot: {α : Type ?u.17177} → [inst : LE α] → α → Prop
IsBot (a: α
a, b: β
b) := fun _: ?m.17224
_ => ⟨ha: IsBot a
ha _: α
_, hb: IsBot b
hb _: β
_⟩
#align is_bot.prod_mk IsBot.prod_mk: ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {a : α} {b : β},
  IsBot a → IsBot b → IsBot (a, b)
IsBot.prod_mk

theorem IsTop.prod_mk: IsTop a → IsTop b → IsTop (a, b)
IsTop.prod_mk (ha: IsTop a
ha : IsTop: {α : Type ?u.17292} → [inst : LE α] → α → Prop
IsTop a: α
a) (hb: IsTop b
hb : IsTop: {α : Type ?u.17319} → [inst : LE α] → α → Prop
IsTop b: β
b) : IsTop: {α : Type ?u.17346} → [inst : LE α] → α → Prop
IsTop (a: α
a, b: β
b) := fun _: ?m.17393
_ => ⟨ha: IsTop a
ha _: α
_, hb: IsTop b
hb _: β
_⟩
#align is_top.prod_mk IsTop.prod_mk: ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {a : α} {b : β},
  IsTop a → IsTop b → IsTop (a, b)
IsTop.prod_mk

theorem IsMin.prod_mk: IsMin a → IsMin b → IsMin (a, b)
IsMin.prod_mk (ha: IsMin a
ha : IsMin: {α : Type ?u.17461} → [inst : LE α] → α → Prop
IsMin a: α
a) (hb: IsMin b
hb : IsMin: {α : Type ?u.17488} → [inst : LE α] → α → Prop
IsMin b: β
b) : IsMin: {α : Type ?u.17515} → [inst : LE α] → α → Prop
IsMin (a: α
a, b: β
b) := fun _: ?m.17562
_ hc: ?m.17565
hc => ⟨ha: IsMin a
ha hc: ?m.17565
hc.1: ∀ {a b : Prop}, a ∧ b → a
1, hb: IsMin b
hb hc: ?m.17565
hc.2: ∀ {a b : Prop}, a ∧ b → b
2⟩
#align is_min.prod_mk IsMin.prod_mk: ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {a : α} {b : β},
  IsMin a → IsMin b → IsMin (a, b)
IsMin.prod_mk

theorem IsMax.prod_mk: IsMax a → IsMax b → IsMax (a, b)
IsMax.prod_mk (ha: IsMax a
ha : IsMax: {α : Type ?u.17640} → [inst : LE α] → α → Prop
IsMax a: α
a) (hb: IsMax b
hb : IsMax: {α : Type ?u.17667} → [inst : LE α] → α → Prop
IsMax b: β
b) : IsMax: {α : Type ?u.17694} → [inst : LE α] → α → Prop
IsMax (a: α
a, b: β
b) := fun _: ?m.17741
_ hc: ?m.17744
hc => ⟨ha: IsMax a
ha hc: ?m.17744
hc.1: ∀ {a b : Prop}, a ∧ b → a
1, hb: IsMax b
hb hc: ?m.17744
hc.2: ∀ {a b : Prop}, a ∧ b → b
2⟩
#align is_max.prod_mk IsMax.prod_mk: ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {a : α} {b : β},
  IsMax a → IsMax b → IsMax (a, b)
IsMax.prod_mk

theorem IsBot.fst: IsBot x → IsBot x.fst
IsBot.fst (hx: IsBot x
hx : IsBot: {α : Type ?u.17819} → [inst : LE α] → α → Prop
IsBot x: α × β
x) : IsBot: {α : Type ?u.17868} → [inst : LE α] → α → Prop
IsBot x: α × β
x.1: {α : Type ?u.17884} → {β : Type ?u.17883} → α × β → α
1 := fun c: ?m.17896
c => (hx: IsBot x
hx (c: ?m.17896
c, x: α × β
x.2: {α : Type ?u.17905} → {β : Type ?u.17904} → α × β → β
2)).1: ∀ {a b : Prop}, a ∧ b → a
1
#align is_bot.fst IsBot.fst: ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {x : α × β}, IsBot x → IsBot x.fst
IsBot.fst

theorem IsBot.snd: IsBot x → IsBot x.snd
IsBot.snd (hx: IsBot x
hx : IsBot: {α : Type ?u.17956} → [inst : LE α] → α → Prop
IsBot x: α × β
x) : IsBot: {α : Type ?u.18005} → [inst : LE α] → α → Prop
IsBot x: α × β
x.2: {α : Type ?u.18021} → {β : Type ?u.18020} → α × β → β
2 := fun c: ?m.18033
c => (hx: IsBot x
hx (x: α × β
x.1: {α : Type ?u.18042} → {β : Type ?u.18041} → α × β → α
1, c: ?m.18033
c)).2: ∀ {a b : Prop}, a ∧ b → b
2
#align is_bot.snd IsBot.snd: ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {x : α × β}, IsBot x → IsBot x.snd
IsBot.snd

theorem IsTop.fst: ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {x : α × β}, IsTop x → IsTop x.fst
IsTop.fst (hx: IsTop x
hx : IsTop: {α : Type ?u.18093} → [inst : LE α] → α → Prop
IsTop x: α × β
x) : IsTop: {α : Type ?u.18142} → [inst : LE α] → α → Prop
IsTop x: α × β
x.1: {α : Type ?u.18158} → {β : Type ?u.18157} → α × β → α
1 := fun c: ?m.18170
c => (hx: IsTop x
hx (c: ?m.18170
c, x: α × β
x.2: {α : Type ?u.18179} → {β : Type ?u.18178} → α × β → β
2)).1: ∀ {a b : Prop}, a ∧ b → a
1
#align is_top.fst IsTop.fst: ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {x : α × β}, IsTop x → IsTop x.fst
IsTop.fst

theorem IsTop.snd: IsTop x → IsTop x.snd
IsTop.snd (hx: IsTop x
hx : IsTop: {α : Type ?u.18230} → [inst : LE α] → α → Prop
IsTop x: α × β
x) : IsTop: {α : Type ?u.18279} → [inst : LE α] → α → Prop
IsTop x: α × β
x.2: {α : Type ?u.18295} → {β : Type ?u.18294} → α × β → β
2 := fun c: ?m.18307
c => (hx: IsTop x
hx (x: α × β
x.1: {α : Type ?u.18316} → {β : Type ?u.18315} → α × β → α
1, c: ?m.18307
c)).2: ∀ {a b : Prop}, a ∧ b → b
2
#align is_top.snd IsTop.snd: ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {x : α × β}, IsTop x → IsTop x.snd
IsTop.snd

theorem IsMin.fst: IsMin x → IsMin x.fst
IsMin.fst (hx: IsMin x
hx : IsMin: {α : Type ?u.18367} → [inst : LE α] → α → Prop
IsMin x: α × β
x) : IsMin: {α : Type ?u.18416} → [inst : LE α] → α → Prop
IsMin x: α × β
x.1: {α : Type ?u.18432} → {β : Type ?u.18431} → α × β → α
1 :=
  fun c: ?m.18444
c hc: ?m.18447
hc => (hx: IsMin x
hx <| show (c: ?m.18444
c, x: α × β
x.2: {α : Type ?u.18457} → {β : Type ?u.18456} → α × β → β
2) ≤ x: α × β
x from (and_iff_left: ∀ {b a : Prop}, b → (a ∧ b ↔ a)
and_iff_left le_rfl: ∀ {α : Type ?u.18502} [inst : Preorder α] {a : α}, a ≤ a
le_rfl).2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 hc: ?m.18447
hc).1: ∀ {a b : Prop}, a ∧ b → a
1
#align is_min.fst IsMin.fst: ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {x : α × β}, IsMin x → IsMin x.fst
IsMin.fst

theorem IsMin.snd: IsMin x → IsMin x.snd
IsMin.snd (hx: IsMin x
hx : IsMin: {α : Type ?u.18589} → [inst : LE α] → α → Prop
IsMin x: α × β
x) : IsMin: {α : Type ?u.18638} → [inst : LE α] → α → Prop
IsMin x: α × β
x.2: {α : Type ?u.18654} → {β : Type ?u.18653} → α × β → β
2 :=
  fun c: ?m.18666
c hc: ?m.18669
hc => (hx: IsMin x
hx <| show (x: α × β
x.1: {α : Type ?u.18679} → {β : Type ?u.18678} → α × β → α
1, c: ?m.18666
c) ≤ x: α × β
x from (and_iff_right: ∀ {a b : Prop}, a → (a ∧ b ↔ b)
and_iff_right le_rfl: ∀ {α : Type ?u.18724} [inst : Preorder α] {a : α}, a ≤ a
le_rfl).2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 hc: ?m.18669
hc).2: ∀ {a b : Prop}, a ∧ b → b
2
#align is_min.snd IsMin.snd: ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {x : α × β}, IsMin x → IsMin x.snd
IsMin.snd

theorem IsMax.fst: IsMax x → IsMax x.fst
IsMax.fst (hx: IsMax x
hx : IsMax: {α : Type ?u.18811} → [inst : LE α] → α → Prop
IsMax x: α × β
x) : IsMax: {α : Type ?u.18860} → [inst : LE α] → α → Prop
IsMax x: α × β
x.1: {α : Type ?u.18876} → {β : Type ?u.18875} → α × β → α
1 :=
  fun c: ?m.18888
c hc: ?m.18891
hc => (hx: IsMax x
hx <| show x: α × β
x ≤ (c: ?m.18888
c, x: α × β
x.2: {α : Type ?u.18901} → {β : Type ?u.18900} → α × β → β
2) from (and_iff_left: ∀ {b a : Prop}, b → (a ∧ b ↔ a)
and_iff_left le_rfl: ∀ {α : Type ?u.18946} [inst : Preorder α] {a : α}, a ≤ a
le_rfl).2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 hc: ?m.18891
hc).1: ∀ {a b : Prop}, a ∧ b → a
1
#align is_max.fst IsMax.fst: ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {x : α × β}, IsMax x → IsMax x.fst
IsMax.fst

theorem IsMax.snd: IsMax x → IsMax x.snd
IsMax.snd (hx: IsMax x
hx : IsMax: {α : Type ?u.19033} → [inst : LE α] → α → Prop
IsMax x: α × β
x) : IsMax: {α : Type ?u.19082} → [inst : LE α] → α → Prop
IsMax x: α × β
x.2: {α : Type ?u.19098} → {β : Type ?u.19097} → α × β → β
2 :=
  fun c: ?m.19110
c hc: ?m.19113
hc => (hx: IsMax x
hx <| show x: α × β
x ≤ (x: α × β
x.1: {α : Type ?u.19123} → {β : Type ?u.19122} → α × β → α
1, c: ?m.19110
c) from (and_iff_right: ∀ {a b : Prop}, a → (a ∧ b ↔ b)
and_iff_right le_rfl: ∀ {α : Type ?u.19168} [inst : Preorder α] {a : α}, a ≤ a
le_rfl).2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 hc: ?m.19113
hc).2: ∀ {a b : Prop}, a ∧ b → b
2
#align is_max.snd IsMax.snd: ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {x : α × β}, IsMax x → IsMax x.snd
IsMax.snd

theorem Prod.isBot_iff: IsBot x ↔ IsBot x.fst ∧ IsBot x.snd
Prod.isBot_iff : IsBot: {α : Type ?u.19255} → [inst : LE α] → α → Prop
IsBot x: α × β
x ↔ IsBot: {α : Type ?u.19290} → [inst : LE α] → α → Prop
IsBot x: α × β
x.1: {α : Type ?u.19294} → {β : Type ?u.19293} → α × β → α
1 ∧ IsBot: {α : Type ?u.19302} → [inst : LE α] → α → Prop
IsBot x: α × β
x.2: {α : Type ?u.19306} → {β : Type ?u.19305} → α × β → β
2 :=
  ⟨fun hx: ?m.19324
hx => ⟨hx: ?m.19324
hx.fst: ∀ {α : Type ?u.19334} {β : Type ?u.19335} [inst : Preorder α] [inst_1 : Preorder β] {x : α × β}, IsBot x → IsBot x.fst
fst, hx: ?m.19324
hx.snd: ∀ {α : Type ?u.19369} {β : Type ?u.19370} [inst : Preorder α] [inst_1 : Preorder β] {x : α × β}, IsBot x → IsBot x.snd
snd⟩, fun h: ?m.19392
h => h: ?m.19392
h.1: ∀ {a b : Prop}, a ∧ b → a
1.prod_mk: ∀ {α : Type ?u.19397} {β : Type ?u.19398} [inst : Preorder α] [inst_1 : Preorder β] {a : α} {b : β},
  IsBot a → IsBot b → IsBot (a, b)
prod_mk h: ?m.19392
h.2: ∀ {a b : Prop}, a ∧ b → b
2⟩
#align prod.is_bot_iff Prod.isBot_iff: ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {x : α × β},
  IsBot x ↔ IsBot x.fst ∧ IsBot x.snd
Prod.isBot_iff

theorem Prod.isTop_iff: IsTop x ↔ IsTop x.fst ∧ IsTop x.snd
Prod.isTop_iff : IsTop: {α : Type ?u.19475} → [inst : LE α] → α → Prop
IsTop x: α × β
x ↔ IsTop: {α : Type ?u.19510} → [inst : LE α] → α → Prop
IsTop x: α × β
x.1: {α : Type ?u.19514} → {β : Type ?u.19513} → α × β → α
1 ∧ IsTop: {α : Type ?u.19522} → [inst : LE α] → α → Prop
IsTop x: α × β
x.2: {α : Type ?u.19526} → {β : Type ?u.19525} → α × β → β
2 :=
  ⟨fun hx: ?m.19544
hx => ⟨hx: ?m.19544
hx.fst: ∀ {α : Type ?u.19554} {β : Type ?u.19555} [inst : Preorder α] [inst_1 : Preorder β] {x : α × β}, IsTop x → IsTop x.fst
fst, hx: ?m.19544
hx.snd: ∀ {α : Type ?u.19589} {β : Type ?u.19590} [inst : Preorder α] [inst_1 : Preorder β] {x : α × β}, IsTop x → IsTop x.snd
snd⟩, fun h: ?m.19612
h => h: ?m.19612
h.1: ∀ {a b : Prop}, a ∧ b → a
1.prod_mk: ∀ {α : Type ?u.19617} {β : Type ?u.19618} [inst : Preorder α] [inst_1 : Preorder β] {a : α} {b : β},
  IsTop a → IsTop b → IsTop (a, b)
prod_mk h: ?m.19612
h.2: ∀ {a b : Prop}, a ∧ b → b
2⟩
#align prod.is_top_iff Prod.isTop_iff: ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {x : α × β},
  IsTop x ↔ IsTop x.fst ∧ IsTop x.snd
Prod.isTop_iff

theorem Prod.isMin_iff: IsMin x ↔ IsMin x.fst ∧ IsMin x.snd
Prod.isMin_iff : IsMin: {α : Type ?u.19695} → [inst : LE α] → α → Prop
IsMin x: α × β
x ↔ IsMin: {α : Type ?u.19730} → [inst : LE α] → α → Prop
IsMin x: α × β
x.1: {α : Type ?u.19734} → {β : Type ?u.19733} → α × β → α
1 ∧ IsMin: {α : Type ?u.19742} → [inst : LE α] → α → Prop
IsMin x: α × β
x.2: {α : Type ?u.19746} → {β : Type ?u.19745} → α × β → β
2 :=
  ⟨fun hx: ?m.19764
hx => ⟨hx: ?m.19764
hx.fst: ∀ {α : Type ?u.19774} {β : Type ?u.19775} [inst : Preorder α] [inst_1 : Preorder β] {x : α × β}, IsMin x → IsMin x.fst
fst, hx: ?m.19764
hx.snd: ∀ {α : Type ?u.19809} {β : Type ?u.19810} [inst : Preorder α] [inst_1 : Preorder β] {x : α × β}, IsMin x → IsMin x.snd
snd⟩, fun h: ?m.19832
h => h: ?m.19832
h.1: ∀ {a b : Prop}, a ∧ b → a
1.prod_mk: ∀ {α : Type ?u.19836} {β : Type ?u.19837} [inst : Preorder α] [inst_1 : Preorder β] {a : α} {b : β},
  IsMin a → IsMin b → IsMin (a, b)
prod_mk h: ?m.19832
h.2: ∀ {a b : Prop}, a ∧ b → b
2⟩
#align prod.is_min_iff Prod.isMin_iff: ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {x : α × β},
  IsMin x ↔ IsMin x.fst ∧ IsMin x.snd
Prod.isMin_iff

theorem Prod.isMax_iff: ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {x : α × β},
  IsMax x ↔ IsMax x.fst ∧ IsMax x.snd
Prod.isMax_iff : IsMax: {α : Type ?u.19914} → [inst : LE α] → α → Prop
IsMax x: α × β
x ↔ IsMax: {α : Type ?u.19949} → [inst : LE α] → α → Prop
IsMax x: α × β
x.1: {α : Type ?u.19953} → {β : Type ?u.19952} → α × β → α
1 ∧ IsMax: {α : Type ?u.19961} → [inst : LE α] → α → Prop
IsMax x: α × β
x.2: {α : Type ?u.19965} → {β : Type ?u.19964} → α × β → β
2 :=
  ⟨fun hx: ?m.19983
hx => ⟨hx: ?m.19983
hx.fst: ∀ {α : Type ?u.19993} {β : Type ?u.19994} [inst : Preorder α] [inst_1 : Preorder β] {x : α × β}, IsMax x → IsMax x.fst
fst, hx: ?m.19983
hx.snd: ∀ {α : Type ?u.20028} {β : Type ?u.20029} [inst : Preorder α] [inst_1 : Preorder β] {x : α × β}, IsMax x → IsMax x.snd
snd⟩, fun h: ?m.20051
h => h: ?m.20051
h.1: ∀ {a b : Prop}, a ∧ b → a
1.prod_mk: ∀ {α : Type ?u.20055} {β : Type ?u.20056} [inst : Preorder α] [inst_1 : Preorder β] {a : α} {b : β},
  IsMax a → IsMax b → IsMax (a, b)
prod_mk h: ?m.20051
h.2: ∀ {a b : Prop}, a ∧ b → b
2⟩
#align prod.is_max_iff Prod.isMax_iff: ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {x : α × β},
  IsMax x ↔ IsMax x.fst ∧ IsMax x.snd
Prod.isMax_iff

end Prod