# mathlib3documentation

order.complete_lattice

# Theory of complete lattices #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

## Main definitions #

• `Sup` and `Inf` are the supremum and the infimum of a set;
• `supr (f : ι → α)` and `infi (f : ι → α)` are indexed supremum and infimum of a function, defined as `Sup` and `Inf` of the range of this function;
• `class complete_lattice`: a bounded lattice such that `Sup s` is always the least upper boundary of `s` and `Inf s` is always the greatest lower boundary of `s`;
• `class complete_linear_order`: a linear ordered complete lattice.

## Naming conventions #

In lemma names,

• `Sup` is called `Sup`
• `Inf` is called `Inf`
• `⨆ i, s i` is called `supr`
• `⨅ i, s i` is called `infi`
• `⨆ i j, s i j` is called `supr₂`. This is a `supr` inside a `supr`.
• `⨅ i j, s i j` is called `infi₂`. This is an `infi` inside an `infi`.
• `⨆ i ∈ s, t i` is called `bsupr` for "bounded `supr`". This is the special case of `supr₂` where `j : i ∈ s`.
• `⨅ i ∈ s, t i` is called `binfi` for "bounded `infi`". This is the special case of `infi₂` where `j : i ∈ s`.

## Notation #

• `⨆ i, f i` : `supr f`, the supremum of the range of `f`;
• `⨅ i, f i` : `infi f`, the infimum of the range of `f`.
@[class]
structure has_Sup (α : Type u_9) :
Type u_9

class for the `Sup` operator

Instances of this typeclass
Instances of other typeclasses for `has_Sup`
• has_Sup.has_sizeof_inst
@[class]
structure has_Inf (α : Type u_9) :
Type u_9

class for the `Inf` operator

Instances of this typeclass
Instances of other typeclasses for `has_Inf`
• has_Inf.has_sizeof_inst
def supr {α : Type u_1} [has_Sup α] {ι : Sort u_2} (s : ι α) :
α

Indexed supremum

Equations
Instances for `↥supr`
def infi {α : Type u_1} [has_Inf α] {ι : Sort u_2} (s : ι α) :
α

Indexed infimum

Equations
Instances for `infi`
@[protected, instance]
def has_Inf_to_nonempty (α : Type u_1) [has_Inf α] :
@[protected, instance]
def has_Sup_to_nonempty (α : Type u_1) [has_Sup α] :
@[protected, instance]
def order_dual.has_Sup (α : Type u_1) [has_Inf α] :
Equations
@[protected, instance]
def order_dual.has_Inf (α : Type u_1) [has_Sup α] :
Equations
@[class]
structure complete_semilattice_Sup (α : Type u_9) :
Type u_9

Note that we rarely use `complete_semilattice_Sup` (in fact, any such object is always a `complete_lattice`, so it's usually best to start there).

Nevertheless it is sometimes a useful intermediate step in constructions.

Instances of this typeclass
Instances of other typeclasses for `complete_semilattice_Sup`
• complete_semilattice_Sup.has_sizeof_inst
@[instance]
theorem le_Sup {α : Type u_1} {s : set α} {a : α} :
a s a
theorem Sup_le {α : Type u_1} {s : set α} {a : α} :
( (b : α), b s b a) a
theorem is_lub_Sup {α : Type u_1} (s : set α) :
theorem is_lub.Sup_eq {α : Type u_1} {s : set α} {a : α} (h : a) :
= a
theorem le_Sup_of_le {α : Type u_1} {s : set α} {a b : α} (hb : b s) (h : a b) :
a
theorem Sup_le_Sup {α : Type u_1} {s t : set α} (h : s t) :
@[simp]
theorem Sup_le_iff {α : Type u_1} {s : set α} {a : α} :
a (b : α), b s b a
theorem le_Sup_iff {α : Type u_1} {s : set α} {a : α} :
a (b : α), a b
theorem le_supr_iff {α : Type u_1} {ι : Sort u_5} {a : α} {s : ι α} :
a supr s (b : α), ( (i : ι), s i b) a b
theorem Sup_le_Sup_of_forall_exists_le {α : Type u_1} {s t : set α} (h : (x : α), x s ( (y : α) (H : y t), x y)) :
theorem Sup_singleton {α : Type u_1} {a : α} :
@[instance]
@[class]
structure complete_semilattice_Inf (α : Type u_9) :
Type u_9

Note that we rarely use `complete_semilattice_Inf` (in fact, any such object is always a `complete_lattice`, so it's usually best to start there).

Nevertheless it is sometimes a useful intermediate step in constructions.

Instances of this typeclass
Instances of other typeclasses for `complete_semilattice_Inf`
• complete_semilattice_Inf.has_sizeof_inst
theorem Inf_le {α : Type u_1} {s : set α} {a : α} :
a s a
theorem le_Inf {α : Type u_1} {s : set α} {a : α} :
( (b : α), b s a b) a
theorem is_glb_Inf {α : Type u_1} (s : set α) :
theorem is_glb.Inf_eq {α : Type u_1} {s : set α} {a : α} (h : a) :
= a
theorem Inf_le_of_le {α : Type u_1} {s : set α} {a b : α} (hb : b s) (h : b a) :
a
theorem Inf_le_Inf {α : Type u_1} {s t : set α} (h : s t) :
@[simp]
theorem le_Inf_iff {α : Type u_1} {s : set α} {a : α} :
a (b : α), b s a b
theorem Inf_le_iff {α : Type u_1} {s : set α} {a : α} :
a (b : α), b a
theorem infi_le_iff {α : Type u_1} {ι : Sort u_5} {a : α} {s : ι α} :
infi s a (b : α), ( (i : ι), b s i) b a
theorem Inf_le_Inf_of_forall_exists_le {α : Type u_1} {s t : set α} (h : (x : α), x s ( (y : α) (H : y t), y x)) :
theorem Inf_singleton {α : Type u_1} {a : α} :
@[class]
structure complete_lattice (α : Type u_9) :
Type u_9

A complete lattice is a bounded lattice which has suprema and infima for every subset.

Instances of this typeclass
Instances of other typeclasses for `complete_lattice`
• complete_lattice.has_sizeof_inst
@[instance]
def complete_lattice.to_lattice (α : Type u_9) [self : complete_lattice α] :
@[instance]
@[instance]
def complete_lattice.to_has_top (α : Type u_9) [self : complete_lattice α] :
@[instance]
@[instance]
def complete_lattice.to_has_bot (α : Type u_9) [self : complete_lattice α] :
@[protected, instance]
Equations
def complete_lattice_of_Inf (α : Type u_1) [H1 : partial_order α] [H2 : has_Inf α] (is_glb_Inf : (s : set α), (has_Inf.Inf s)) :

Create a `complete_lattice` from a `partial_order` and `Inf` function that returns the greatest lower bound of a set. Usually this constructor provides poor definitional equalities. If other fields are known explicitly, they should be provided; for example, if `inf` is known explicitly, construct the `complete_lattice` instance as

``````instance : complete_lattice my_T :=
{ inf := better_inf,
le_inf := ...,
inf_le_right := ...,
inf_le_left := ...
-- don't care to fix sup, Sup, bot, top
..complete_lattice_of_Inf my_T _ }
``````
Equations

Any `complete_semilattice_Inf` is in fact a `complete_lattice`.

Note that this construction has bad definitional properties: see the doc-string on `complete_lattice_of_Inf`.

Equations
def complete_lattice_of_Sup (α : Type u_1) [H1 : partial_order α] [H2 : has_Sup α] (is_lub_Sup : (s : set α), (has_Sup.Sup s)) :

Create a `complete_lattice` from a `partial_order` and `Sup` function that returns the least upper bound of a set. Usually this constructor provides poor definitional equalities. If other fields are known explicitly, they should be provided; for example, if `inf` is known explicitly, construct the `complete_lattice` instance as

``````instance : complete_lattice my_T :=
{ inf := better_inf,
le_inf := ...,
inf_le_right := ...,
inf_le_left := ...
-- don't care to fix sup, Inf, bot, top
..complete_lattice_of_Sup my_T _ }
``````
Equations

Any `complete_semilattice_Sup` is in fact a `complete_lattice`.

Note that this construction has bad definitional properties: see the doc-string on `complete_lattice_of_Sup`.

Equations
@[class]
structure complete_linear_order (α : Type u_9) :
Type u_9

A complete linear order is a linear order whose lattice structure is complete.

Instances of this typeclass
Instances of other typeclasses for `complete_linear_order`
• complete_linear_order.has_sizeof_inst
@[instance]
@[protected, instance]
def order_dual.complete_lattice (α : Type u_1)  :
Equations
@[protected, instance]
Equations
@[simp]
theorem to_dual_Sup {α : Type u_1} (s : set α) :
@[simp]
theorem to_dual_Inf {α : Type u_1} (s : set α) :
@[simp]
theorem of_dual_Sup {α : Type u_1} (s : set αᵒᵈ) :
@[simp]
theorem of_dual_Inf {α : Type u_1} (s : set αᵒᵈ) :
@[simp]
theorem to_dual_supr {α : Type u_1} {ι : Sort u_5} (f : ι α) :
order_dual.to_dual ( (i : ι), f i) = (i : ι), order_dual.to_dual (f i)
@[simp]
theorem to_dual_infi {α : Type u_1} {ι : Sort u_5} (f : ι α) :
order_dual.to_dual ( (i : ι), f i) = (i : ι), order_dual.to_dual (f i)
@[simp]
theorem of_dual_supr {α : Type u_1} {ι : Sort u_5} (f : ι αᵒᵈ) :
order_dual.of_dual ( (i : ι), f i) = (i : ι), order_dual.of_dual (f i)
@[simp]
theorem of_dual_infi {α : Type u_1} {ι : Sort u_5} (f : ι αᵒᵈ) :
order_dual.of_dual ( (i : ι), f i) = (i : ι), order_dual.of_dual (f i)
theorem Inf_le_Sup {α : Type u_1} {s : set α} (hs : s.nonempty) :
theorem Sup_union {α : Type u_1} {s t : set α} :
theorem Inf_union {α : Type u_1} {s t : set α} :
theorem Sup_inter_le {α : Type u_1} {s t : set α} :
theorem le_Inf_inter {α : Type u_1} {s t : set α} :
@[simp]
theorem Sup_empty {α : Type u_1}  :
@[simp]
theorem Inf_empty {α : Type u_1}  :
@[simp]
theorem Sup_univ {α : Type u_1}  :
@[simp]
theorem Inf_univ {α : Type u_1}  :
@[simp]
theorem Sup_insert {α : Type u_1} {a : α} {s : set α} :
= a
@[simp]
theorem Inf_insert {α : Type u_1} {a : α} {s : set α} :
= a
theorem Sup_le_Sup_of_subset_insert_bot {α : Type u_1} {s t : set α} (h : s ) :
theorem Inf_le_Inf_of_subset_insert_top {α : Type u_1} {s t : set α} (h : s ) :
@[simp]
theorem Sup_diff_singleton_bot {α : Type u_1} (s : set α) :
@[simp]
theorem Inf_diff_singleton_top {α : Type u_1} (s : set α) :
theorem Sup_pair {α : Type u_1} {a b : α} :
has_Sup.Sup {a, b} = a b
theorem Inf_pair {α : Type u_1} {a b : α} :
has_Inf.Inf {a, b} = a b
@[simp]
theorem Sup_eq_bot {α : Type u_1} {s : set α} :
(a : α), a s a =
@[simp]
theorem Inf_eq_top {α : Type u_1} {s : set α} :
(a : α), a s a =
theorem eq_singleton_bot_of_Sup_eq_bot_of_nonempty {α : Type u_1} {s : set α} (h_sup : = ) (hne : s.nonempty) :
s = {}
theorem Sup_eq_of_forall_le_of_forall_lt_exists_gt {α : Type u_1} {s : set α} {b : α} (h₁ : (a : α), a s a b) (h₂ : (w : α), w < b ( (a : α) (H : a s), w < a)) :
= b

Introduction rule to prove that `b` is the supremum of `s`: it suffices to check that `b` is larger than all elements of `s`, and that this is not the case of any `w < b`. See `cSup_eq_of_forall_le_of_forall_lt_exists_gt` for a version in conditionally complete lattices.

theorem Inf_eq_of_forall_ge_of_forall_gt_exists_lt {α : Type u_1} {s : set α} {b : α} :
( (a : α), a s b a) ( (w : α), b < w ( (a : α) (H : a s), a < w)) = b

Introduction rule to prove that `b` is the infimum of `s`: it suffices to check that `b` is smaller than all elements of `s`, and that this is not the case of any `w > b`. See `cInf_eq_of_forall_ge_of_forall_gt_exists_lt` for a version in conditionally complete lattices.

theorem lt_Sup_iff {α : Type u_1} {s : set α} {b : α} :
b < (a : α) (H : a s), b < a
theorem Inf_lt_iff {α : Type u_1} {s : set α} {b : α} :
< b (a : α) (H : a s), a < b
theorem Sup_eq_top {α : Type u_1} {s : set α} :
(b : α), b < ( (a : α) (H : a s), b < a)
theorem Inf_eq_bot {α : Type u_1} {s : set α} :
(b : α), b > ( (a : α) (H : a s), a < b)
theorem lt_supr_iff {α : Type u_1} {ι : Sort u_5} {a : α} {f : ι α} :
a < supr f (i : ι), a < f i
theorem infi_lt_iff {α : Type u_1} {ι : Sort u_5} {a : α} {f : ι α} :
infi f < a (i : ι), f i < a
theorem Sup_range {α : Type u_1} {ι : Sort u_5} [has_Sup α] {f : ι α} :
= supr f
theorem Sup_eq_supr' {α : Type u_1} [has_Sup α] (s : set α) :
= (a : s), a
theorem supr_congr {α : Type u_1} {ι : Sort u_5} [has_Sup α] {f g : ι α} (h : (i : ι), f i = g i) :
( (i : ι), f i) = (i : ι), g i
theorem function.surjective.supr_comp {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} [has_Sup α] {f : ι ι'} (hf : function.surjective f) (g : ι' α) :
( (x : ι), g (f x)) = (y : ι'), g y
theorem equiv.supr_comp {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} [has_Sup α] {g : ι' α} (e : ι ι') :
( (x : ι), g (e x)) = (y : ι'), g y
@[protected]
theorem function.surjective.supr_congr {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} [has_Sup α] {f : ι α} {g : ι' α} (h : ι ι') (h1 : function.surjective h) (h2 : (x : ι), g (h x) = f x) :
( (x : ι), f x) = (y : ι'), g y
@[protected]
theorem equiv.supr_congr {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} [has_Sup α] {f : ι α} {g : ι' α} (e : ι ι') (h : (x : ι), g (e x) = f x) :
( (x : ι), f x) = (y : ι'), g y
theorem supr_congr_Prop {α : Type u_1} [has_Sup α] {p q : Prop} {f₁ : p α} {f₂ : q α} (pq : p q) (f : (x : q), f₁ _ = f₂ x) :
supr f₁ = supr f₂
theorem supr_plift_up {α : Type u_1} {ι : Sort u_5} [has_Sup α] (f : α) :
( (i : ι), f {down := i}) = (i : plift ι), f i
theorem supr_plift_down {α : Type u_1} {ι : Sort u_5} [has_Sup α] (f : ι α) :
( (i : plift ι), f i.down) = (i : ι), f i
theorem supr_range' {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [has_Sup α] (g : β α) (f : ι β) :
( (b : (set.range f)), g b) = (i : ι), g (f i)
theorem Sup_image' {α : Type u_1} {β : Type u_2} [has_Sup α] {s : set β} {f : β α} :
has_Sup.Sup (f '' s) = (a : s), f a
theorem Inf_range {α : Type u_1} {ι : Sort u_5} [has_Inf α] {f : ι α} :
= infi f
theorem Inf_eq_infi' {α : Type u_1} [has_Inf α] (s : set α) :
= (a : s), a
theorem infi_congr {α : Type u_1} {ι : Sort u_5} [has_Inf α] {f g : ι α} (h : (i : ι), f i = g i) :
( (i : ι), f i) = (i : ι), g i
theorem function.surjective.infi_comp {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} [has_Inf α] {f : ι ι'} (hf : function.surjective f) (g : ι' α) :
( (x : ι), g (f x)) = (y : ι'), g y
theorem equiv.infi_comp {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} [has_Inf α] {g : ι' α} (e : ι ι') :
( (x : ι), g (e x)) = (y : ι'), g y
@[protected]
theorem function.surjective.infi_congr {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} [has_Inf α] {f : ι α} {g : ι' α} (h : ι ι') (h1 : function.surjective h) (h2 : (x : ι), g (h x) = f x) :
( (x : ι), f x) = (y : ι'), g y
@[protected]
theorem equiv.infi_congr {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} [has_Inf α] {f : ι α} {g : ι' α} (e : ι ι') (h : (x : ι), g (e x) = f x) :
( (x : ι), f x) = (y : ι'), g y
theorem infi_congr_Prop {α : Type u_1} [has_Inf α] {p q : Prop} {f₁ : p α} {f₂ : q α} (pq : p q) (f : (x : q), f₁ _ = f₂ x) :
infi f₁ = infi f₂
theorem infi_plift_up {α : Type u_1} {ι : Sort u_5} [has_Inf α] (f : α) :
( (i : ι), f {down := i}) = (i : plift ι), f i
theorem infi_plift_down {α : Type u_1} {ι : Sort u_5} [has_Inf α] (f : ι α) :
( (i : plift ι), f i.down) = (i : ι), f i
theorem infi_range' {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [has_Inf α] (g : β α) (f : ι β) :
( (b : (set.range f)), g b) = (i : ι), g (f i)
theorem Inf_image' {α : Type u_1} {β : Type u_2} [has_Inf α] {s : set β} {f : β α} :
has_Inf.Inf (f '' s) = (a : s), f a
theorem le_supr {α : Type u_1} {ι : Sort u_5} (f : ι α) (i : ι) :
f i supr f
theorem infi_le {α : Type u_1} {ι : Sort u_5} (f : ι α) (i : ι) :
infi f f i
theorem le_supr' {α : Type u_1} {ι : Sort u_5} (f : ι α) (i : ι) :
(:f i supr f:)
theorem infi_le' {α : Type u_1} {ι : Sort u_5} (f : ι α) (i : ι) :
(:infi f f i:)
theorem is_lub_supr {α : Type u_1} {ι : Sort u_5} {f : ι α} :
is_lub (set.range f) ( (j : ι), f j)
theorem is_glb_infi {α : Type u_1} {ι : Sort u_5} {f : ι α} :
is_glb (set.range f) ( (j : ι), f j)
theorem is_lub.supr_eq {α : Type u_1} {ι : Sort u_5} {f : ι α} {a : α} (h : is_lub (set.range f) a) :
( (j : ι), f j) = a
theorem is_glb.infi_eq {α : Type u_1} {ι : Sort u_5} {f : ι α} {a : α} (h : is_glb (set.range f) a) :
( (j : ι), f j) = a
theorem le_supr_of_le {α : Type u_1} {ι : Sort u_5} {f : ι α} {a : α} (i : ι) (h : a f i) :
a supr f
theorem infi_le_of_le {α : Type u_1} {ι : Sort u_5} {f : ι α} {a : α} (i : ι) (h : f i a) :
infi f a
theorem le_supr₂ {α : Type u_1} {ι : Sort u_5} {κ : ι Sort u_7} {f : Π (i : ι), κ i α} (i : ι) (j : κ i) :
f i j (i : ι) (j : κ i), f i j
theorem infi₂_le {α : Type u_1} {ι : Sort u_5} {κ : ι Sort u_7} {f : Π (i : ι), κ i α} (i : ι) (j : κ i) :
( (i : ι) (j : κ i), f i j) f i j
theorem le_supr₂_of_le {α : Type u_1} {ι : Sort u_5} {κ : ι Sort u_7} {a : α} {f : Π (i : ι), κ i α} (i : ι) (j : κ i) (h : a f i j) :
a (i : ι) (j : κ i), f i j
theorem infi₂_le_of_le {α : Type u_1} {ι : Sort u_5} {κ : ι Sort u_7} {a : α} {f : Π (i : ι), κ i α} (i : ι) (j : κ i) (h : f i j a) :
( (i : ι) (j : κ i), f i j) a
theorem supr_le {α : Type u_1} {ι : Sort u_5} {f : ι α} {a : α} (h : (i : ι), f i a) :
supr f a
theorem le_infi {α : Type u_1} {ι : Sort u_5} {f : ι α} {a : α} (h : (i : ι), a f i) :
a infi f
theorem supr₂_le {α : Type u_1} {ι : Sort u_5} {κ : ι Sort u_7} {a : α} {f : Π (i : ι), κ i α} (h : (i : ι) (j : κ i), f i j a) :
( (i : ι) (j : κ i), f i j) a
theorem le_infi₂ {α : Type u_1} {ι : Sort u_5} {κ : ι Sort u_7} {a : α} {f : Π (i : ι), κ i α} (h : (i : ι) (j : κ i), a f i j) :
a (i : ι) (j : κ i), f i j
theorem supr₂_le_supr {α : Type u_1} {ι : Sort u_5} (κ : ι Sort u_2) (f : ι α) :
( (i : ι) (j : κ i), f i) (i : ι), f i
theorem infi_le_infi₂ {α : Type u_1} {ι : Sort u_5} (κ : ι Sort u_2) (f : ι α) :
( (i : ι), f i) (i : ι) (j : κ i), f i
theorem supr_mono {α : Type u_1} {ι : Sort u_5} {f g : ι α} (h : (i : ι), f i g i) :
theorem infi_mono {α : Type u_1} {ι : Sort u_5} {f g : ι α} (h : (i : ι), f i g i) :
theorem supr₂_mono {α : Type u_1} {ι : Sort u_5} {κ : ι Sort u_7} {f g : Π (i : ι), κ i α} (h : (i : ι) (j : κ i), f i j g i j) :
( (i : ι) (j : κ i), f i j) (i : ι) (j : κ i), g i j
theorem infi₂_mono {α : Type u_1} {ι : Sort u_5} {κ : ι Sort u_7} {f g : Π (i : ι), κ i α} (h : (i : ι) (j : κ i), f i j g i j) :
( (i : ι) (j : κ i), f i j) (i : ι) (j : κ i), g i j
theorem supr_mono' {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} {f : ι α} {g : ι' α} (h : (i : ι), (i' : ι'), f i g i') :
theorem infi_mono' {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} {f : ι α} {g : ι' α} (h : (i' : ι'), (i : ι), f i g i') :
theorem supr₂_mono' {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} {κ : ι Sort u_7} {κ' : ι' Sort u_8} {f : Π (i : ι), κ i α} {g : Π (i' : ι'), κ' i' α} (h : (i : ι) (j : κ i), (i' : ι') (j' : κ' i'), f i j g i' j') :
( (i : ι) (j : κ i), f i j) (i : ι') (j : κ' i), g i j
theorem infi₂_mono' {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} {κ : ι Sort u_7} {κ' : ι' Sort u_8} {f : Π (i : ι), κ i α} {g : Π (i' : ι'), κ' i' α} (h : (i : ι') (j : κ' i), (i' : ι) (j' : κ i'), f i' j' g i j) :
( (i : ι) (j : κ i), f i j) (i : ι') (j : κ' i), g i j
theorem supr_const_mono {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} {a : α} (h : ι ι') :
( (i : ι), a) (j : ι'), a
theorem infi_const_mono {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} {a : α} (h : ι' ι) :
( (i : ι), a) (j : ι'), a
theorem supr_infi_le_infi_supr {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} (f : ι ι' α) :
( (i : ι), (j : ι'), f i j) (j : ι'), (i : ι), f i j
theorem bsupr_mono {α : Type u_1} {ι : Sort u_5} {f : ι α} {p q : ι Prop} (hpq : (i : ι), p i q i) :
( (i : ι) (h : p i), f i) (i : ι) (h : q i), f i
theorem binfi_mono {α : Type u_1} {ι : Sort u_5} {f : ι α} {p q : ι Prop} (hpq : (i : ι), p i q i) :
( (i : ι) (h : q i), f i) (i : ι) (h : p i), f i
@[simp]
theorem supr_le_iff {α : Type u_1} {ι : Sort u_5} {f : ι α} {a : α} :
supr f a (i : ι), f i a
@[simp]
theorem le_infi_iff {α : Type u_1} {ι : Sort u_5} {f : ι α} {a : α} :
a infi f (i : ι), a f i
@[simp]
theorem supr₂_le_iff {α : Type u_1} {ι : Sort u_5} {κ : ι Sort u_7} {a : α} {f : Π (i : ι), κ i α} :
( (i : ι) (j : κ i), f i j) a (i : ι) (j : κ i), f i j a
@[simp]
theorem le_infi₂_iff {α : Type u_1} {ι : Sort u_5} {κ : ι Sort u_7} {a : α} {f : Π (i : ι), κ i α} :
(a (i : ι) (j : κ i), f i j) (i : ι) (j : κ i), a f i j
theorem supr_lt_iff {α : Type u_1} {ι : Sort u_5} {f : ι α} {a : α} :
supr f < a (b : α), b < a (i : ι), f i b
theorem lt_infi_iff {α : Type u_1} {ι : Sort u_5} {f : ι α} {a : α} :
a < infi f (b : α), a < b (i : ι), b f i
theorem Sup_eq_supr {α : Type u_1} {s : set α} :
= (a : α) (H : a s), a
theorem Inf_eq_infi {α : Type u_1} {s : set α} :
= (a : α) (H : a s), a
theorem monotone.le_map_supr {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {s : ι α} {f : α β} (hf : monotone f) :
( (i : ι), f (s i)) f (supr s)
theorem antitone.le_map_infi {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {s : ι α} {f : α β} (hf : antitone f) :
( (i : ι), f (s i)) f (infi s)
theorem monotone.le_map_supr₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {κ : ι Sort u_7} {f : α β} (hf : monotone f) (s : Π (i : ι), κ i α) :
( (i : ι) (j : κ i), f (s i j)) f ( (i : ι) (j : κ i), s i j)
theorem antitone.le_map_infi₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {κ : ι Sort u_7} {f : α β} (hf : antitone f) (s : Π (i : ι), κ i α) :
( (i : ι) (j : κ i), f (s i j)) f ( (i : ι) (j : κ i), s i j)
theorem monotone.le_map_Sup {α : Type u_1} {β : Type u_2} {s : set α} {f : α β} (hf : monotone f) :
( (a : α) (H : a s), f a) f (has_Sup.Sup s)
theorem antitone.le_map_Inf {α : Type u_1} {β : Type u_2} {s : set α} {f : α β} (hf : antitone f) :
( (a : α) (H : a s), f a) f (has_Inf.Inf s)
theorem order_iso.map_supr {α : Type u_1} {β : Type u_2} {ι : Sort u_5} (f : α ≃o β) (x : ι α) :
f ( (i : ι), x i) = (i : ι), f (x i)
theorem order_iso.map_infi {α : Type u_1} {β : Type u_2} {ι : Sort u_5} (f : α ≃o β) (x : ι α) :
f ( (i : ι), x i) = (i : ι), f (x i)
theorem order_iso.map_Sup {α : Type u_1} {β : Type u_2} (f : α ≃o β) (s : set α) :
f (has_Sup.Sup s) = (a : α) (H : a s), f a
theorem order_iso.map_Inf {α : Type u_1} {β : Type u_2} (f : α ≃o β) (s : set α) :
f (has_Inf.Inf s) = (a : α) (H : a s), f a
theorem supr_comp_le {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_2} (f : ι' α) (g : ι ι') :
( (x : ι), f (g x)) (y : ι'), f y
theorem le_infi_comp {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_2} (f : ι' α) (g : ι ι') :
( (y : ι'), f y) (x : ι), f (g x)
theorem monotone.supr_comp_eq {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [preorder β] {f : β α} (hf : monotone f) {s : ι β} (hs : (x : β), (i : ι), x s i) :
( (x : ι), f (s x)) = (y : β), f y
theorem monotone.infi_comp_eq {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [preorder β] {f : β α} (hf : monotone f) {s : ι β} (hs : (x : β), (i : ι), s i x) :
( (x : ι), f (s x)) = (y : β), f y
theorem antitone.map_supr_le {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {s : ι α} {f : α β} (hf : antitone f) :
f (supr s) (i : ι), f (s i)
theorem monotone.map_infi_le {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {s : ι α} {f : α β} (hf : monotone f) :
f (infi s) (i : ι), f (s i)
theorem antitone.map_supr₂_le {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {κ : ι Sort u_7} {f : α β} (hf : antitone f) (s : Π (i : ι), κ i α) :
f ( (i : ι) (j : κ i), s i j) (i : ι) (j : κ i), f (s i j)
theorem monotone.map_infi₂_le {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {κ : ι Sort u_7} {f : α β} (hf : monotone f) (s : Π (i : ι), κ i α) :
f ( (i : ι) (j : κ i), s i j) (i : ι) (j : κ i), f (s i j)
theorem antitone.map_Sup_le {α : Type u_1} {β : Type u_2} {s : set α} {f : α β} (hf : antitone f) :
f (has_Sup.Sup s) (a : α) (H : a s), f a
theorem monotone.map_Inf_le {α : Type u_1} {β : Type u_2} {s : set α} {f : α β} (hf : monotone f) :
f (has_Inf.Inf s) (a : α) (H : a s), f a
theorem supr_const_le {α : Type u_1} {ι : Sort u_5} {a : α} :
( (i : ι), a) a
theorem le_infi_const {α : Type u_1} {ι : Sort u_5} {a : α} :
a (i : ι), a
theorem supr_const {α : Type u_1} {ι : Sort u_5} {a : α} [nonempty ι] :
( (b : ι), a) = a
theorem infi_const {α : Type u_1} {ι : Sort u_5} {a : α} [nonempty ι] :
( (b : ι), a) = a
@[simp]
theorem supr_bot {α : Type u_1} {ι : Sort u_5}  :
( (i : ι), ) =
@[simp]
theorem infi_top {α : Type u_1} {ι : Sort u_5}  :
( (i : ι), ) =
@[simp]
theorem supr_eq_bot {α : Type u_1} {ι : Sort u_5} {s : ι α} :
supr s = (i : ι), s i =
@[simp]
theorem infi_eq_top {α : Type u_1} {ι : Sort u_5} {s : ι α} :
infi s = (i : ι), s i =
@[simp]
theorem supr₂_eq_bot {α : Type u_1} {ι : Sort u_5} {κ : ι Sort u_7} {f : Π (i : ι), κ i α} :
( (i : ι) (j : κ i), f i j) = (i : ι) (j : κ i), f i j =
@[simp]
theorem infi₂_eq_top {α : Type u_1} {ι : Sort u_5} {κ : ι Sort u_7} {f : Π (i : ι), κ i α} :
( (i : ι) (j : κ i), f i j) = (i : ι) (j : κ i), f i j =
@[simp]
theorem supr_pos {α : Type u_1} {p : Prop} {f : p α} (hp : p) :
( (h : p), f h) = f hp
@[simp]
theorem infi_pos {α : Type u_1} {p : Prop} {f : p α} (hp : p) :
( (h : p), f h) = f hp
@[simp]
theorem supr_neg {α : Type u_1} {p : Prop} {f : p α} (hp : ¬p) :
( (h : p), f h) =
@[simp]
theorem infi_neg {α : Type u_1} {p : Prop} {f : p α} (hp : ¬p) :
( (h : p), f h) =
theorem supr_eq_of_forall_le_of_forall_lt_exists_gt {α : Type u_1} {ι : Sort u_5} {b : α} {f : ι α} (h₁ : (i : ι), f i b) (h₂ : (w : α), w < b ( (i : ι), w < f i)) :
( (i : ι), f i) = b

Introduction rule to prove that `b` is the supremum of `f`: it suffices to check that `b` is larger than `f i` for all `i`, and that this is not the case of any `w<b`. See `csupr_eq_of_forall_le_of_forall_lt_exists_gt` for a version in conditionally complete lattices.

theorem infi_eq_of_forall_ge_of_forall_gt_exists_lt {α : Type u_1} {ι : Sort u_5} {f : ι α} {b : α} :
( (i : ι), b f i) ( (w : α), b < w ( (i : ι), f i < w)) ( (i : ι), f i) = b

Introduction rule to prove that `b` is the infimum of `f`: it suffices to check that `b` is smaller than `f i` for all `i`, and that this is not the case of any `w>b`. See `cinfi_eq_of_forall_ge_of_forall_gt_exists_lt` for a version in conditionally complete lattices.

theorem supr_eq_dif {α : Type u_1} {p : Prop} [decidable p] (a : p α) :
( (h : p), a h) = dite p (λ (h : p), a h) (λ (h : ¬p), )
theorem supr_eq_if {α : Type u_1} {p : Prop} [decidable p] (a : α) :
( (h : p), a) = ite p a
theorem infi_eq_dif {α : Type u_1} {p : Prop} [decidable p] (a : p α) :
( (h : p), a h) = dite p (λ (h : p), a h) (λ (h : ¬p), )
theorem infi_eq_if {α : Type u_1} {p : Prop} [decidable p] (a : α) :
( (h : p), a) = ite p a
theorem supr_comm {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} {f : ι ι' α} :
( (i : ι) (j : ι'), f i j) = (j : ι') (i : ι), f i j
theorem infi_comm {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} {f : ι ι' α} :
( (i : ι) (j : ι'), f i j) = (j : ι') (i : ι), f i j
theorem supr₂_comm {α : Type u_1} {ι₁ : Sort u_2} {ι₂ : Sort u_3} {κ₁ : ι₁ Sort u_4} {κ₂ : ι₂ Sort u_5} (f : Π (i₁ : ι₁), κ₁ i₁ Π (i₂ : ι₂), κ₂ i₂ α) :
( (i₁ : ι₁) (j₁ : κ₁ i₁) (i₂ : ι₂) (j₂ : κ₂ i₂), f i₁ j₁ i₂ j₂) = (i₂ : ι₂) (j₂ : κ₂ i₂) (i₁ : ι₁) (j₁ : κ₁ i₁), f i₁ j₁ i₂ j₂
theorem infi₂_comm {α : Type u_1} {ι₁ : Sort u_2} {ι₂ : Sort u_3} {κ₁ : ι₁ Sort u_4} {κ₂ : ι₂ Sort u_5} (f : Π (i₁ : ι₁), κ₁ i₁ Π (i₂ : ι₂), κ₂ i₂ α) :
( (i₁ : ι₁) (j₁ : κ₁ i₁) (i₂ : ι₂) (j₂ : κ₂ i₂), f i₁ j₁ i₂ j₂) = (i₂ : ι₂) (j₂ : κ₂ i₂) (i₁ : ι₁) (j₁ : κ₁ i₁), f i₁ j₁ i₂ j₂
@[simp]
theorem supr_supr_eq_left {α : Type u_1} {β : Type u_2} {b : β} {f : Π (x : β), x = b α} :
( (x : β) (h : x = b), f x h) = f b rfl
@[simp]
theorem infi_infi_eq_left {α : Type u_1} {β : Type u_2} {b : β} {f : Π (x : β), x = b α} :
( (x : β) (h : x = b), f x h) = f b rfl
@[simp]
theorem supr_supr_eq_right {α : Type u_1} {β : Type u_2} {b : β} {f : Π (x : β), b = x α} :
( (x : β) (h : b = x), f x h) = f b rfl
@[simp]
theorem infi_infi_eq_right {α : Type u_1} {β : Type u_2} {b : β} {f : Π (x : β), b = x α} :
( (x : β) (h : b = x), f x h) = f b rfl
theorem supr_subtype {α : Type u_1} {ι : Sort u_5} {p : ι Prop} {f : α} :
supr f = (i : ι) (h : p i), f i, h⟩
theorem infi_subtype {α : Type u_1} {ι : Sort u_5} {p : ι Prop} {f : α} :
infi f = (i : ι) (h : p i), f i, h⟩
theorem supr_subtype' {α : Type u_1} {ι : Sort u_5} {p : ι Prop} {f : Π (i : ι), p i α} :
( (i : ι) (h : p i), f i h) = (x : subtype p), f x _
theorem infi_subtype' {α : Type u_1} {ι : Sort u_5} {p : ι Prop} {f : Π (i : ι), p i α} :
( (i : ι) (h : p i), f i h) = (x : subtype p), f x _
theorem supr_subtype'' {α : Type u_1} {ι : Type u_2} (s : set ι) (f : ι α) :
( (i : s), f i) = (t : ι) (H : t s), f t
theorem infi_subtype'' {α : Type u_1} {ι : Type u_2} (s : set ι) (f : ι α) :
( (i : s), f i) = (t : ι) (H : t s), f t
theorem bsupr_const {α : Type u_1} {ι : Type u_2} {a : α} {s : set ι} (hs : s.nonempty) :
( (i : ι) (H : i s), a) = a
theorem binfi_const {α : Type u_1} {ι : Type u_2} {a : α} {s : set ι} (hs : s.nonempty) :
( (i : ι) (H : i s), a) = a
theorem supr_sup_eq {α : Type u_1} {ι : Sort u_5} {f g : ι α} :
( (x : ι), f x g x) = ( (x : ι), f x) (x : ι), g x
theorem infi_inf_eq {α : Type u_1} {ι : Sort u_5} {f g : ι α} :
( (x : ι), f x g x) = ( (x : ι), f x) (x : ι), g x
theorem supr_sup {α : Type u_1} {ι : Sort u_5} [nonempty ι] {f : ι α} {a : α} :
( (x : ι), f x) a = (x : ι), f x a
theorem infi_inf {α : Type u_1} {ι : Sort u_5} [nonempty ι] {f : ι α} {a : α} :
( (x : ι), f x) a = (x : ι), f x a
theorem sup_supr {α : Type u_1} {ι : Sort u_5} [nonempty ι] {f : ι α} {a : α} :
(a (x : ι), f x) = (x : ι), a f x
theorem inf_infi {α : Type u_1} {ι : Sort u_5} [nonempty ι] {f : ι α} {a : α} :
(a (x : ι), f x) = (x : ι), a f x
theorem bsupr_sup {α : Type u_1} {ι : Sort u_5} {p : ι Prop} {f : Π (i : ι), p i α} {a : α} (h : (i : ι), p i) :
( (i : ι) (h : p i), f i h) a = (i : ι) (h : p i), f i h a
theorem sup_bsupr {α : Type u_1} {ι : Sort u_5} {p : ι Prop} {f : Π (i : ι), p i α} {a : α} (h : (i : ι), p i) :
(a (i : ι) (h : p i), f i h) = (i : ι) (h : p i), a f i h
theorem binfi_inf {α : Type u_1} {ι : Sort u_5} {p : ι Prop} {f : Π (i : ι), p i α} {a : α} (h : (i : ι), p i) :
( (i : ι) (h : p i), f i h) a = (i : ι) (h : p i), f i h a
theorem inf_binfi {α : Type u_1} {ι : Sort u_5} {p : ι Prop} {f : Π (i : ι), p i α} {a : α} (h : (i : ι), p i) :
(a (i : ι) (h : p i), f i h) = (i : ι) (h : p i), a f i h

### `supr` and `infi` under `Prop`#

@[simp]
theorem supr_false {α : Type u_1} {s : false α} :
@[simp]
theorem infi_false {α : Type u_1} {s : false α} :
theorem supr_true {α : Type u_1} {s : true α} :
supr s =
theorem infi_true {α : Type u_1} {s : true α} :
infi s =
@[simp]
theorem supr_exists {α : Type u_1} {ι : Sort u_5} {p : ι Prop} {f : α} :
( (x : Exists p), f x) = (i : ι) (h : p i), f _
@[simp]
theorem infi_exists {α : Type u_1} {ι : Sort u_5} {p : ι Prop} {f : α} :
( (x : Exists p), f x) = (i : ι) (h : p i), f _
theorem supr_and {α : Type u_1} {p q : Prop} {s : p q α} :
supr s = (h₁ : p) (h₂ : q), s _
theorem infi_and {α : Type u_1} {p q : Prop} {s : p q α} :
infi s = (h₁ : p) (h₂ : q), s _
theorem supr_and' {α : Type u_1} {p q : Prop} {s : p q α} :
( (h₁ : p) (h₂ : q), s h₁ h₂) = (h : p q), s _ _

The symmetric case of `supr_and`, useful for rewriting into a supremum over a conjunction

theorem infi_and' {α : Type u_1} {p q : Prop} {s : p q α} :
( (h₁ : p) (h₂ : q), s h₁ h₂) = (h : p q), s _ _

The symmetric case of `infi_and`, useful for rewriting into a infimum over a conjunction

theorem supr_or {α : Type u_1} {p q : Prop} {s : p q α} :
( (x : p q), s x) = ( (i : p), s _) (j : q), s _
theorem infi_or {α : Type u_1} {p q : Prop} {s : p q α} :
( (x : p q), s x) = ( (i : p), s _) (j : q), s _
theorem supr_dite {α : Type u_1} {ι : Sort u_5} (p : ι Prop) (f : Π (i : ι), p i α) (g : Π (i : ι), ¬p i α) :
( (i : ι), dite (p i) (λ (h : p i), f i h) (λ (h : ¬p i), g i h)) = ( (i : ι) (h : p i), f i h) (i : ι) (h : ¬p i), g i h
theorem infi_dite {α : Type u_1} {ι : Sort u_5} (p : ι Prop) (f : Π (i : ι), p i α) (g : Π (i : ι), ¬p i α) :
( (i : ι), dite (p i) (λ (h : p i), f i h) (λ (h : ¬p i), g i h)) = ( (i : ι) (h : p i), f i h) (i : ι) (h : ¬p i), g i h
theorem supr_ite {α : Type u_1} {ι : Sort u_5} (p : ι Prop) (f g : ι α) :
( (i : ι), ite (p i) (f i) (g i)) = ( (i : ι) (h : p i), f i) (i : ι) (h : ¬p i), g i
theorem infi_ite {α : Type u_1} {ι : Sort u_5} (p : ι Prop) (f g : ι α) :
( (i : ι), ite (p i) (f i) (g i)) = ( (i : ι) (h : p i), f i) (i : ι) (h : ¬p i), g i
theorem supr_range {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {g : β α} {f : ι β} :
( (b : β) (H : b , g b) = (i : ι), g (f i)
theorem infi_range {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {g : β α} {f : ι β} :
( (b : β) (H : b , g b) = (i : ι), g (f i)
theorem Sup_image {α : Type u_1} {β : Type u_2} {s : set β} {f : β α} :
has_Sup.Sup (f '' s) = (a : β) (H : a s), f a
theorem Inf_image {α : Type u_1} {β : Type u_2} {s : set β} {f : β α} :
has_Inf.Inf (f '' s) = (a : β) (H : a s), f a
theorem supr_emptyset {α : Type u_1} {β : Type u_2} {f : β α} :
( (x : β) (H : x ), f x) =
theorem infi_emptyset {α : Type u_1} {β : Type u_2} {f : β α} :
( (x : β) (H : x ), f x) =
theorem supr_univ {α : Type u_1} {β : Type u_2} {f : β α} :
( (x : β) (H : , f x) = (x : β), f x
theorem infi_univ {α : Type u_1} {β : Type u_2} {f : β α} :
( (x : β) (H : , f x) = (x : β), f x
theorem supr_union {α : Type u_1} {β : Type u_2} {f : β α} {s t : set β} :
( (x : β) (H : x s t), f x) = ( (x : β) (H : x s), f x) (x : β) (H : x t), f x
theorem infi_union {α : Type u_1} {β : Type u_2} {f : β α} {s t : set β} :
( (x : β) (H : x s t), f x) = ( (x : β) (H : x s), f x) (x : β) (H : x t), f x
theorem supr_split {α : Type u_1} {β : Type u_2} (f : β α) (p : β Prop) :
( (i : β), f i) = ( (i : β) (h : p i), f i) (i : β) (h : ¬p i), f i
theorem infi_split {α : Type u_1} {β : Type u_2} (f : β α) (p : β Prop) :
( (i : β), f i) = ( (i : β) (h : p i), f i) (i : β) (h : ¬p i), f i
theorem supr_split_single {α : Type u_1} {β : Type u_2} (f : β α) (i₀ : β) :
( (i : β), f i) = f i₀ (i : β) (h : i i₀), f i
theorem infi_split_single {α : Type u_1} {β : Type u_2} (f : β α) (i₀ : β) :
( (i : β), f i) = f i₀ (i : β) (h : i i₀), f i
theorem supr_le_supr_of_subset {α : Type u_1} {β : Type u_2} {f : β α} {s t : set β} :
s t (( (x : β) (H : x s), f x) (x : β) (H : x t), f x)
theorem infi_le_infi_of_subset {α : Type u_1} {β : Type u_2} {f : β α} {s t : set β} :
s t (( (x : β) (H : x t), f x) (x : β) (H : x s), f x)
theorem supr_insert {α : Type u_1} {β : Type u_2} {f : β α} {s : set β} {b : β} :
( (x : β) (H : x , f x) = f b (x : β) (H : x s), f x
theorem infi_insert {α : Type u_1} {β : Type u_2} {f : β α} {s : set β} {b : β} :
( (x : β) (H : x , f x) = f b (x : β) (H : x s), f x
theorem supr_singleton {α : Type u_1} {β : Type u_2} {f : β α} {b : β} :
( (x : β) (H : x {b}), f x) = f b
theorem infi_singleton {α : Type u_1} {β : Type u_2} {f : β α} {b : β} :
( (x : β) (H : x {b}), f x) = f b
theorem supr_pair {α : Type u_1} {β : Type u_2} {f : β α} {a b : β} :
( (x : β) (H : x {a, b}), f x) = f a f b
theorem infi_pair {α : Type u_1} {β : Type u_2} {f : β α} {a b : β} :
( (x : β) (H : x {a, b}), f x) = f a f b
theorem supr_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : β γ} {g : γ α} {t : set β} :
( (c : γ) (H : c f '' t), g c) = (b : β) (H : b t), g (f b)
theorem infi_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : β γ} {g : γ α} {t : set β} :
( (c : γ) (H : c f '' t), g c) = (b : β) (H : b t), g (f b)
theorem supr_extend_bot {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {e : ι β} (he : function.injective e) (f : ι α) :
( (j : β), j) = (i : ι), f i
theorem infi_extend_top {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {e : ι β} (he : function.injective e) (f : ι α) :
( (j : β), j) = infi f

### `supr` and `infi` under `Type`#

theorem supr_of_empty' {α : Type u_1} {ι : Sort u_2} [has_Sup α] [is_empty ι] (f : ι α) :
theorem infi_of_empty' {α : Type u_1} {ι : Sort u_2} [has_Inf α] [is_empty ι] (f : ι α) :
theorem supr_of_empty {α : Type u_1} {ι : Sort u_5} [is_empty ι] (f : ι α) :
theorem infi_of_empty {α : Type u_1} {ι : Sort u_5} [is_empty ι] (f : ι α) :
theorem supr_bool_eq {α : Type u_1} {f : bool α} :
( (b : bool), f b) =
theorem infi_bool_eq {α : Type u_1} {f : bool α} :
( (b : bool), f b) =
theorem sup_eq_supr {α : Type u_1} (x y : α) :
x y = (b : bool), cond b x y
theorem inf_eq_infi {α : Type u_1} (x y : α) :
x y = (b : bool), cond b x y
theorem is_glb_binfi {α : Type u_1} {β : Type u_2} {s : set β} {f : β α} :
is_glb (f '' s) ( (x : β) (H : x s), f x)
theorem is_lub_bsupr {α : Type u_1} {β : Type u_2} {s : set β} {f : β α} :
is_lub (f '' s) ( (x : β) (H : x s), f x)
theorem supr_sigma {α : Type u_1} {β : Type u_2} {p : β Type u_3} {f : α} :
( (x : sigma p), f x) = (i : β) (j : p i), f i, j⟩
theorem infi_sigma {α : Type u_1} {β : Type u_2} {p : β Type u_3} {f : α} :
( (x : sigma p), f x) = (i : β) (j : p i), f i, j⟩
theorem supr_prod {α : Type u_1} {β : Type u_2} {γ : Type u_4} {f : β × γ α} :
( (x : β × γ), f x) = (i : β) (j : γ), f (i, j)
theorem infi_prod {α : Type u_1} {β : Type u_2} {γ : Type u_4} {f : β × γ α} :
( (x : β × γ), f x) = (i : β) (j : γ), f (i, j)
theorem bsupr_prod {α : Type u_1} {β : Type u_2} {γ : Type u_4} {f : β × γ α} {s : set β} {t : set γ} :
( (x : β × γ) (H : x s ×ˢ t), f x) = (a : β) (H : a s) (b : γ) (H : b t), f (a, b)
theorem binfi_prod {α : Type u_1} {β : Type u_2} {γ : Type u_4} {f : β × γ α} {s : set β} {t : set γ} :
( (x : β × γ) (H : x s ×ˢ t), f x) = (a : β) (H : a s) (b : γ) (H : b t), f (a, b)
theorem supr_sum {α : Type u_1} {β : Type u_2} {γ : Type u_4} {f : β γ α} :
( (x : β γ), f x) = ( (i : β), f (sum.inl i)) (j : γ), f (sum.inr j)
theorem infi_sum {α : Type u_1} {β : Type u_2} {γ : Type u_4} {f : β γ α} :
( (x : β γ), f x) = ( (i : β), f (sum.inl i)) (j : γ), f (sum.inr j)
theorem supr_option {α : Type u_1} {β : Type u_2} (f : α) :
( (o : option β), f o) = (b : β), f (option.some b)
theorem infi_option {α : Type u_1} {β : Type u_2} (f : α) :
( (o : option β), f o) = (b : β), f (option.some b)
theorem supr_option_elim {α : Type u_1} {β : Type u_2} (a : α) (f : β α) :
( (o : option β), f o) = a (b : β), f b

A version of `supr_option` useful for rewriting right-to-left.

theorem infi_option_elim {α : Type u_1} {β : Type u_2} (a : α) (f : β α) :
( (o : option β), f o) = a (b : β), f b

A version of `infi_option` useful for rewriting right-to-left.

theorem supr_ne_bot_subtype {α : Type u_1} {ι : Sort u_5} (f : ι α) :
( (i : {i // f i }), f i) = (i : ι), f i

When taking the supremum of `f : ι → α`, the elements of `ι` on which `f` gives `⊥` can be dropped, without changing the result.

theorem infi_ne_top_subtype {α : Type u_1} {ι : Sort u_5} (f : ι α) :
( (i : {i // f i }), f i) = (i : ι), f i

When taking the infimum of `f : ι → α`, the elements of `ι` on which `f` gives `⊤` can be dropped, without changing the result.

theorem Sup_image2 {α : Type u_1} {β : Type u_2} {γ : Type u_4} {f : β γ α} {s : set β} {t : set γ} :
has_Sup.Sup s t) = (a : β) (H : a s) (b : γ) (H : b t), f a b
theorem Inf_image2 {α : Type u_1} {β : Type u_2} {γ : Type u_4} {f : β γ α} {s : set β} {t : set γ} :
has_Inf.Inf s t) = (a : β) (H : a s) (b : γ) (H : b t), f a b

### `supr` and `infi` under `ℕ`#

theorem supr_ge_eq_supr_nat_add {α : Type u_1} (u : α) (n : ) :
( (i : ) (H : i n), u i) = (i : ), u (i + n)
theorem infi_ge_eq_infi_nat_add {α : Type u_1} (u : α) (n : ) :
( (i : ) (H : i n), u i) = (i : ), u (i + n)
theorem monotone.supr_nat_add {α : Type u_1} {f : α} (hf : monotone f) (k : ) :
( (n : ), f (n + k)) = (n : ), f n
theorem antitone.infi_nat_add {α : Type u_1} {f : α} (hf : antitone f) (k : ) :
( (n : ), f (n + k)) = (n : ), f n
@[simp]
theorem supr_infi_ge_nat_add {α : Type u_1} (f : α) (k : ) :
( (n : ), (i : ) (H : i n), f (i + k)) = (n : ), (i : ) (H : i n), f i
@[simp]
theorem infi_supr_ge_nat_add {α : Type u_1} (f : α) (k : ) :
( (n : ), (i : ) (H : i n), f (i + k)) = (n : ), (i : ) (H : i n), f i
theorem sup_supr_nat_succ {α : Type u_1} (u : α) :
(u 0 (i : ), u (i + 1)) = (i : ), u i
theorem inf_infi_nat_succ {α : Type u_1} (u : α) :
(u 0 (i : ), u (i + 1)) = (i : ), u i
theorem infi_nat_gt_zero_eq {α : Type u_1} (f : α) :
( (i : ) (H : i > 0), f i) = (i : ), f (i + 1)
theorem supr_nat_gt_zero_eq {α : Type u_1} (f : α) :
( (i : ) (H : i > 0), f i) = (i : ), f (i + 1)
theorem supr_eq_top {α : Type u_1} {ι : Sort u_5} (f : ι α) :
supr f = (b : α), b < ( (i : ι), b < f i)
theorem infi_eq_bot {α : Type u_1} {ι : Sort u_5} (f : ι α) :
infi f = (b : α), b > ( (i : ι), f i < b)

### Instances #

@[protected, instance]
Equations
@[protected, instance]
noncomputable def Prop.complete_linear_order  :
Equations
@[simp]
theorem Sup_Prop_eq {s : set Prop} :
= (p : Prop) (H : p s), p
@[simp]
theorem Inf_Prop_eq {s : set Prop} :
= (p : Prop), p s p
@[simp]
theorem supr_Prop_eq {ι : Sort u_5} {p : ι Prop} :
( (i : ι), p i) = (i : ι), p i
@[simp]
theorem infi_Prop_eq {ι : Sort u_5} {p : ι Prop} :
( (i : ι), p i) = (i : ι), p i
@[protected, instance]
def pi.has_Sup {α : Type u_1} {β : α Type u_2} [Π (i : α), has_Sup (β i)] :
has_Sup (Π (i : α), β i)
Equations
@[protected, instance]
def pi.has_Inf {α : Type u_1} {β : α Type u_2} [Π (i : α), has_Inf (β i)] :
has_Inf (Π (i : α), β i)
Equations
@[protected, instance]
def pi.complete_lattice {α : Type u_1} {β : α Type u_2} [Π (i : α), complete_lattice (β i)] :
complete_lattice (Π (i : α), β i)
Equations
theorem Sup_apply {α : Type u_1} {β : α Type u_2} [Π (i : α), has_Sup (β i)] {s : set (Π (a : α), β a)} {a : α} :
a = (f : s), f a
theorem Inf_apply {α : Type u_1} {β : α Type u_2} [Π (i : α), has_Inf (β i)] {s : set (Π (a : α), β a)} {a : α} :
a = (f : s), f a
@[simp]
theorem supr_apply {α : Type u_1} {β : α Type u_2} {ι : Sort u_3} [Π (i : α), has_Sup (β i)] {f : ι Π (a : α), β a} {a : α} :
( (i : ι), f i) a = (i : ι), f i a
@[simp]
theorem infi_apply {α : Type u_1} {β : α Type u_2} {ι : Sort u_3} [Π (i : α), has_Inf (β i)] {f : ι Π (a : α), β a} {a : α} :
( (i : ι), f i) a = (i : ι), f i a
theorem unary_relation_Sup_iff {α : Type u_1} (s : set Prop)) {a : α} :
a (r : α Prop), r s r a
theorem unary_relation_Inf_iff {α : Type u_1} (s : set Prop)) {a : α} :
a (r : α Prop), r s r a
theorem binary_relation_Sup_iff {α : Type u_1} {β : Type u_2} (s : set β Prop)) {a : α} {b : β} :
a b (r : α β Prop), r s r a b
theorem binary_relation_Inf_iff {α : Type u_1} {β : Type u_2} (s : set β Prop)) {a : α} {b : β} :
a b (r : α β Prop), r s r a b
theorem monotone_Sup_of_monotone {α : Type u_1} {β : Type u_2} [preorder α] {s : set β)} (m_s : (f : α β), f s ) :
theorem monotone_Inf_of_monotone {α : Type u_1} {β : Type u_2} [preorder α] {s : set β)} (m_s : (f : α β), f s ) :
@[protected, instance]
def prod.has_Sup (α : Type u_1) (β : Type u_2) [has_Sup α] [has_Sup β] :
has_Sup × β)
Equations
@[protected, instance]
def prod.has_Inf (α : Type u_1) (β : Type u_2) [has_Inf α] [has_Inf β] :
has_Inf × β)
Equations
theorem prod.fst_Inf {α : Type u_1} {β : Type u_2} [has_Inf α] [has_Inf β] (s : set × β)) :
theorem prod.snd_Inf {α : Type u_1} {β : Type u_2} [has_Inf α] [has_Inf β] (s : set × β)) :
theorem prod.swap_Inf {α : Type u_1} {β : Type u_2} [has_Inf α] [has_Inf β] (s : set × β)) :
theorem prod.fst_Sup {α : Type u_1} {β : Type u_2} [has_Sup α] [has_Sup β] (s : set × β)) :
theorem prod.snd_Sup {α : Type u_1} {β : Type u_2} [has_Sup α] [has_Sup β] (s : set × β)) :
theorem prod.swap_Sup {α : Type u_1} {β : Type u_2} [has_Sup α] [has_Sup β] (s : set × β)) :
theorem prod.fst_infi {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [has_Inf α] [has_Inf β] (f : ι α × β) :
(infi f).fst = (i : ι), (f i).fst
theorem prod.snd_infi {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [has_Inf α] [has_Inf β] (f : ι α × β) :
(infi f).snd = (i : ι), (f i).snd
theorem prod.swap_infi {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [has_Inf α] [has_Inf β] (f : ι α × β) :
(infi f).swap = (i : ι), (f i).swap
theorem prod.infi_mk {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [has_Inf α] [has_Inf β] (f : ι α) (g : ι β) :
( (i : ι), (f i, g i)) = ( (i : ι), f i, (i : ι), g i)
theorem