mathlib documentation

order.complete_lattice

Theory of complete lattices

Main definitions

Naming conventions

We use Sup/Inf/supr/infi for the corresponding functions in the statement. Sometimes we also use bsupr/binfi for "boundedsupremum or infimum, i.e. one of⨆ i ∈ s, f i, ⨆ i (hi : p i), f i, or more generally⨆ i (hi : p i), f i hi`.

Notation

def supr {α : Type u_1} [has_Sup α] {ι : Sort u_2} :
(ι → α) → α

Indexed supremum

Equations
def infi {α : Type u_1} [has_Inf α] {ι : Sort u_2} :
(ι → α) → α

Indexed infimum

Equations
@[instance]
def has_Inf_to_nonempty (α : Type u_1) [has_Inf α] :

@[instance]
def has_Sup_to_nonempty (α : Type u_1) [has_Sup α] :

@[instance]
def order_dual.has_Sup (α : Type u_1) [has_Inf α] :

Equations
@[instance]
def order_dual.has_Inf (α : Type u_1) [has_Sup α] :

Equations
@[instance]
def complete_lattice.to_has_Inf (α : Type u_6) [s : complete_lattice α] :

@[instance]
def complete_lattice.to_has_Sup (α : Type u_6) [s : complete_lattice α] :

@[class]
structure complete_lattice  :
Type u_6Type u_6
  • sup : α → α → α
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a a
  • le_trans : ∀ (a b c_1 : α), a bb c_1a c_1
  • lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a bb aa = b
  • le_sup_left : ∀ (a b : α), a a b
  • le_sup_right : ∀ (a b : α), b a b
  • sup_le : ∀ (a b c_1 : α), a c_1b c_1a b c_1
  • inf : α → α → α
  • inf_le_left : ∀ (a b : α), a b a
  • inf_le_right : ∀ (a b : α), a b b
  • le_inf : ∀ (a b c_1 : α), a ba c_1a b c_1
  • top : α
  • le_top : ∀ (a : α), a
  • bot : α
  • bot_le : ∀ (a : α), a
  • Sup : set α → α
  • Inf : set α → α
  • le_Sup : ∀ (s : set α) (a : α), a sa complete_lattice.Sup s
  • Sup_le : ∀ (s : set α) (a : α), (∀ (b : α), b sb a)complete_lattice.Sup s a
  • Inf_le : ∀ (s : set α) (a : α), a scomplete_lattice.Inf s a
  • le_Inf : ∀ (s : set α) (a : α), (∀ (b : α), b sa b)a complete_lattice.Inf s

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

Instances
@[instance]

def complete_lattice_of_Inf (α : Type u_1) [H1 : partial_order α] [H2 : has_Inf α] :
(∀ (s : set α), is_glb s (Inf s))complete_lattice α

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, so it should be used with .. complete_lattice_of_Inf α _.

Equations
def complete_lattice_of_Sup (α : Type u_1) [H1 : partial_order α] [H2 : has_Sup α] :
(∀ (s : set α), is_lub s (Sup s))complete_lattice α

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, so it should be used with .. complete_lattice_of_Sup α _.

Equations
@[class]
structure complete_linear_order  :
Type u_6Type u_6

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

Instances
theorem le_Sup {α : Type u_1} [complete_lattice α] {s : set α} {a : α} :
a sa Sup s

theorem Sup_le {α : Type u_1} [complete_lattice α] {s : set α} {a : α} :
(∀ (b : α), b sb a)Sup s a

theorem Inf_le {α : Type u_1} [complete_lattice α] {s : set α} {a : α} :
a sInf s a

theorem le_Inf {α : Type u_1} [complete_lattice α] {s : set α} {a : α} :
(∀ (b : α), b sa b)a Inf s

theorem is_lub_Sup {α : Type u_1} [complete_lattice α] (s : set α) :
is_lub s (Sup s)

theorem is_lub.Sup_eq {α : Type u_1} [complete_lattice α] {s : set α} {a : α} :
is_lub s aSup s = a

theorem is_glb_Inf {α : Type u_1} [complete_lattice α] (s : set α) :
is_glb s (Inf s)

theorem is_glb.Inf_eq {α : Type u_1} [complete_lattice α] {s : set α} {a : α} :
is_glb s aInf s = a

theorem le_Sup_of_le {α : Type u_1} [complete_lattice α] {s : set α} {a b : α} :
b sa ba Sup s

theorem Inf_le_of_le {α : Type u_1} [complete_lattice α] {s : set α} {a b : α} :
b sb aInf s a

theorem Sup_le_Sup {α : Type u_1} [complete_lattice α] {s t : set α} :
s tSup s Sup t

theorem Inf_le_Inf {α : Type u_1} [complete_lattice α] {s t : set α} :
s tInf t Inf s

@[simp]
theorem Sup_le_iff {α : Type u_1} [complete_lattice α] {s : set α} {a : α} :
Sup s a ∀ (b : α), b sb a

@[simp]
theorem le_Inf_iff {α : Type u_1} [complete_lattice α] {s : set α} {a : α} :
a Inf s ∀ (b : α), b sa b

theorem Sup_le_Sup_of_forall_exists_le {α : Type u_1} [complete_lattice α] {s t : set α} :
(∀ (x : α), x s(∃ (y : α) (H : y t), x y))Sup s Sup t

theorem Inf_le_Inf_of_forall_exists_le {α : Type u_1} [complete_lattice α] {s t : set α} :
(∀ (x : α), x s(∃ (y : α) (H : y t), y x))Inf t Inf s

theorem Inf_le_Sup {α : Type u_1} [complete_lattice α] {s : set α} :
s.nonemptyInf s Sup s

theorem Sup_union {α : Type u_1} [complete_lattice α] {s t : set α} :
Sup (s t) = Sup s Sup t

theorem Sup_inter_le {α : Type u_1} [complete_lattice α] {s t : set α} :
Sup (s t) Sup s Sup t

theorem Inf_union {α : Type u_1} [complete_lattice α] {s t : set α} :
Inf (s t) = Inf s Inf t

theorem le_Inf_inter {α : Type u_1} [complete_lattice α] {s t : set α} :
Inf s Inf t Inf (s t)

@[simp]
theorem Sup_empty {α : Type u_1} [complete_lattice α] :

@[simp]
theorem Inf_empty {α : Type u_1} [complete_lattice α] :

@[simp]
theorem Sup_univ {α : Type u_1} [complete_lattice α] :

@[simp]
theorem Inf_univ {α : Type u_1} [complete_lattice α] :

@[simp]
theorem Sup_insert {α : Type u_1} [complete_lattice α] {a : α} {s : set α} :
Sup (insert a s) = a Sup s

@[simp]
theorem Inf_insert {α : Type u_1} [complete_lattice α] {a : α} {s : set α} :
Inf (insert a s) = a Inf s

theorem Sup_le_Sup_of_subset_instert_bot {α : Type u_1} [complete_lattice α] {s t : set α} :
s insert tSup s Sup t

theorem Inf_le_Inf_of_subset_insert_top {α : Type u_1} [complete_lattice α] {s t : set α} :
s insert tInf t Inf s

theorem Sup_singleton {α : Type u_1} [complete_lattice α] {a : α} :
Sup {a} = a

theorem Inf_singleton {α : Type u_1} [complete_lattice α] {a : α} :
Inf {a} = a

theorem Sup_pair {α : Type u_1} [complete_lattice α] {a b : α} :
Sup {a, b} = a b

theorem Inf_pair {α : Type u_1} [complete_lattice α] {a b : α} :
Inf {a, b} = a b

@[simp]
theorem Inf_eq_top {α : Type u_1} [complete_lattice α] {s : set α} :
Inf s = ∀ (a : α), a sa =

@[simp]
theorem Sup_eq_bot {α : Type u_1} [complete_lattice α] {s : set α} :
Sup s = ∀ (a : α), a sa =

theorem Inf_lt_iff {α : Type u_1} [complete_linear_order α] {s : set α} {b : α} :
Inf s < b ∃ (a : α) (H : a s), a < b

theorem lt_Sup_iff {α : Type u_1} [complete_linear_order α] {s : set α} {b : α} :
b < Sup s ∃ (a : α) (H : a s), b < a

theorem Sup_eq_top {α : Type u_1} [complete_linear_order α] {s : set α} :
Sup s = ∀ (b : α), b < (∃ (a : α) (H : a s), b < a)

theorem Inf_eq_bot {α : Type u_1} [complete_linear_order α] {s : set α} :
Inf s = ∀ (b : α), b > (∃ (a : α) (H : a s), a < b)

theorem lt_supr_iff {α : Type u_1} {ι : Sort u_4} [complete_linear_order α] {a : α} {f : ι → α} :
a < supr f ∃ (i : ι), a < f i

theorem infi_lt_iff {α : Type u_1} {ι : Sort u_4} [complete_linear_order α] {a : α} {f : ι → α} :
infi f < a ∃ (i : ι), f i < a

theorem le_supr {α : Type u_1} {ι : Sort u_4} [complete_lattice α] (s : ι → α) (i : ι) :
s i supr s

theorem le_supr' {α : Type u_1} {ι : Sort u_4} [complete_lattice α] (s : ι → α) (i : ι) :
(:s i supr s:)

theorem is_lub_supr {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {s : ι → α} :
is_lub (set.range s) (⨆ (j : ι), s j)

theorem is_lub.supr_eq {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {s : ι → α} {a : α} :
is_lub (set.range s) a(⨆ (j : ι), s j) = a

theorem is_glb_infi {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {s : ι → α} :
is_glb (set.range s) (⨅ (j : ι), s j)

theorem is_glb.infi_eq {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {s : ι → α} {a : α} :
is_glb (set.range s) a(⨅ (j : ι), s j) = a

theorem le_supr_of_le {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {s : ι → α} {a : α} (i : ι) :
a s ia supr s

theorem le_bsupr {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {p : ι → Prop} {f : Π (i : ι), p i → α} (i : ι) (hi : p i) :
f i hi ⨆ (i : ι) (hi : p i), f i hi

theorem supr_le {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {s : ι → α} {a : α} :
(∀ (i : ι), s i a)supr s a

theorem bsupr_le {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {a : α} {p : ι → Prop} {f : Π (i : ι), p i → α} :
(∀ (i : ι) (hi : p i), f i hi a)(⨆ (i : ι) (hi : p i), f i hi) a

theorem bsupr_le_supr {α : Type u_1} {ι : Sort u_4} [complete_lattice α] (p : ι → Prop) (f : ι → α) :
(⨆ (i : ι) (H : p i), f i) ⨆ (i : ι), f i

theorem supr_le_supr {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {s t : ι → α} :
(∀ (i : ι), s i t i)supr s supr t

theorem supr_le_supr2 {α : Type u_1} {ι : Sort u_4} {ι₂ : Sort u_5} [complete_lattice α] {s : ι → α} {t : ι₂ → α} :
(∀ (i : ι), ∃ (j : ι₂), s i t j)supr s supr t

theorem bsupr_le_bsupr {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {p : ι → Prop} {f g : Π (i : ι), p i → α} :
(∀ (i : ι) (hi : p i), f i hi g i hi)((⨆ (i : ι) (hi : p i), f i hi) ⨆ (i : ι) (hi : p i), g i hi)

theorem supr_le_supr_const {α : Type u_1} {ι : Sort u_4} {ι₂ : Sort u_5} [complete_lattice α] {a : α} :
(ι → ι₂)((⨆ (i : ι), a) ⨆ (j : ι₂), a)

@[simp]
theorem supr_le_iff {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {s : ι → α} {a : α} :
supr s a ∀ (i : ι), s i a

theorem Sup_eq_supr {α : Type u_1} [complete_lattice α] {s : set α} :
Sup s = ⨆ (a : α) (H : a s), a

theorem le_supr_iff {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {s : ι → α} {a : α} :
a supr s ∀ (b : α), (∀ (i : ι), s i b)a b

theorem monotone.le_map_supr {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [complete_lattice α] {s : ι → α} [complete_lattice β] {f : α → β} :
monotone f(⨆ (i : ι), f (s i)) f (supr s)

theorem monotone.le_map_supr2 {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [complete_lattice α] [complete_lattice β] {f : α → β} (hf : monotone f) {ι' : ι → Sort u_3} (s : Π (i : ι), ι' i → α) :
(⨆ (i : ι) (h : ι' i), f (s i h)) f (⨆ (i : ι) (h : ι' i), s i h)

theorem monotone.le_map_Sup {α : Type u_1} {β : Type u_2} [complete_lattice α] [complete_lattice β] {s : set α} {f : α → β} :
monotone f(⨆ (a : α) (H : a s), f a) f (Sup s)

theorem supr_comp_le {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {ι' : Sort u_2} (f : ι' → α) (g : ι → ι') :
(⨆ (x : ι), f (g x)) ⨆ (y : ι'), f y

theorem monotone.supr_comp_eq {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [complete_lattice α] [preorder β] {f : β → α} (hf : monotone f) {s : ι → β} :
(∀ (x : β), ∃ (i : ι), x s i)((⨆ (x : ι), f (s x)) = ⨆ (y : β), f y)

theorem function.surjective.supr_comp {ι : Sort u_4} {ι₂ : Sort u_5} {α : Type u_1} [has_Sup α] {f : ι → ι₂} (hf : function.surjective f) (g : ι₂ → α) :
(⨆ (x : ι), g (f x)) = ⨆ (y : ι₂), g y

theorem supr_congr {ι : Sort u_4} {ι₂ : Sort u_5} {α : Type u_1} [has_Sup α] {f : ι → α} {g : ι₂ → α} (h : ι → ι₂) :
function.surjective h(∀ (x : ι), g (h 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) :
(∀ (x : q), f₁ _ = f₂ x)supr f₁ = supr f₂

theorem infi_le {α : Type u_1} {ι : Sort u_4} [complete_lattice α] (s : ι → α) (i : ι) :
infi s s i

theorem infi_le' {α : Type u_1} {ι : Sort u_4} [complete_lattice α] (s : ι → α) (i : ι) :
(:infi s s i:)

theorem infi_le_of_le {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {s : ι → α} {a : α} (i : ι) :
s i ainfi s a

theorem binfi_le {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {p : ι → Prop} {f : Π (i : ι), p i → α} (i : ι) (hi : p i) :
(⨅ (i : ι) (hi : p i), f i hi) f i hi

theorem le_infi {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {s : ι → α} {a : α} :
(∀ (i : ι), a s i)a infi s

theorem le_binfi {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {a : α} {p : ι → Prop} {f : Π (i : ι), p i → α} :
(∀ (i : ι) (hi : p i), a f i hi)(a ⨅ (i : ι) (hi : p i), f i hi)

theorem infi_le_binfi {α : Type u_1} {ι : Sort u_4} [complete_lattice α] (p : ι → Prop) (f : ι → α) :
(⨅ (i : ι), f i) ⨅ (i : ι) (H : p i), f i

theorem infi_le_infi {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {s t : ι → α} :
(∀ (i : ι), s i t i)infi s infi t

theorem infi_le_infi2 {α : Type u_1} {ι : Sort u_4} {ι₂ : Sort u_5} [complete_lattice α] {s : ι → α} {t : ι₂ → α} :
(∀ (j : ι₂), ∃ (i : ι), s i t j)infi s infi t

theorem binfi_le_binfi {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {p : ι → Prop} {f g : Π (i : ι), p i → α} :
(∀ (i : ι) (hi : p i), f i hi g i hi)((⨅ (i : ι) (hi : p i), f i hi) ⨅ (i : ι) (hi : p i), g i hi)

theorem infi_le_infi_const {α : Type u_1} {ι : Sort u_4} {ι₂ : Sort u_5} [complete_lattice α] {a : α} :
(ι₂ → ι)((⨅ (i : ι), a) ⨅ (j : ι₂), a)

@[simp]
theorem le_infi_iff {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {s : ι → α} {a : α} :
a infi s ∀ (i : ι), a s i

theorem Inf_eq_infi {α : Type u_1} [complete_lattice α] {s : set α} :
Inf s = ⨅ (a : α) (H : a s), a

theorem monotone.map_infi_le {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [complete_lattice α] {s : ι → α} [complete_lattice β] {f : α → β} :
monotone f(f (infi s) ⨅ (i : ι), f (s i))

theorem monotone.map_infi2_le {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [complete_lattice α] [complete_lattice β] {f : α → β} (hf : monotone f) {ι' : ι → Sort u_3} (s : Π (i : ι), ι' i → α) :
f (⨅ (i : ι) (h : ι' i), s i h) ⨅ (i : ι) (h : ι' i), f (s i h)

theorem monotone.map_Inf_le {α : Type u_1} {β : Type u_2} [complete_lattice α] [complete_lattice β] {s : set α} {f : α → β} :
monotone f(f (Inf s) ⨅ (a : α) (H : a s), f a)

theorem le_infi_comp {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {ι' : Sort u_2} (f : ι' → α) (g : ι → ι') :
(⨅ (y : ι'), f y) ⨅ (x : ι), f (g x)

theorem monotone.infi_comp_eq {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [complete_lattice α] [preorder β] {f : β → α} (hf : monotone f) {s : ι → β} :
(∀ (x : β), ∃ (i : ι), s i x)((⨅ (x : ι), f (s x)) = ⨅ (y : β), f y)

theorem function.surjective.infi_comp {ι : Sort u_4} {ι₂ : Sort u_5} {α : Type u_1} [has_Inf α] {f : ι → ι₂} (hf : function.surjective f) (g : ι₂ → α) :
(⨅ (x : ι), g (f x)) = ⨅ (y : ι₂), g y

theorem infi_congr {ι : Sort u_4} {ι₂ : Sort u_5} {α : Type u_1} [has_Inf α] {f : ι → α} {g : ι₂ → α} (h : ι → ι₂) :
function.surjective h(∀ (x : ι), g (h 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) :
(∀ (x : q), f₁ _ = f₂ x)infi f₁ = infi f₂

theorem infi_const {α : Type u_1} {ι : Sort u_4} [complete_lattice α] [nonempty ι] {a : α} :
(⨅ (b : ι), a) = a

theorem supr_const {α : Type u_1} {ι : Sort u_4} [complete_lattice α] [nonempty ι] {a : α} :
(⨆ (b : ι), a) = a

@[simp]
theorem infi_top {α : Type u_1} {ι : Sort u_4} [complete_lattice α] :
(⨅ (i : ι), ) =

@[simp]
theorem supr_bot {α : Type u_1} {ι : Sort u_4} [complete_lattice α] :
(⨆ (i : ι), ) =

@[simp]
theorem infi_eq_top {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {s : ι → α} :
infi s = ∀ (i : ι), s i =

@[simp]
theorem supr_eq_bot {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {s : ι → α} :
supr s = ∀ (i : ι), s i =

@[simp]
theorem infi_pos {α : Type u_1} [complete_lattice α] {p : Prop} {f : p → α} (hp : p) :
(⨅ (h : p), f h) = f hp

@[simp]
theorem infi_neg {α : Type u_1} [complete_lattice α] {p : Prop} {f : p → α} :
¬p → (⨅ (h : p), f h) =

@[simp]
theorem supr_pos {α : Type u_1} [complete_lattice α] {p : Prop} {f : p → α} (hp : p) :
(⨆ (h : p), f h) = f hp

@[simp]
theorem supr_neg {α : Type u_1} [complete_lattice α] {p : Prop} {f : p → α} :
¬p → (⨆ (h : p), f h) =

theorem supr_eq_dif {α : Type u_1} [complete_lattice α] {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} [complete_lattice α] {p : Prop} [decidable p] (a : α) :
(⨆ (h : p), a) = ite p a

theorem infi_eq_dif {α : Type u_1} [complete_lattice α] {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} [complete_lattice α] {p : Prop} [decidable p] (a : α) :
(⨅ (h : p), a) = ite p a

theorem infi_comm {α : Type u_1} {ι : Sort u_4} {ι₂ : Sort u_5} [complete_lattice α] {f : ι → ι₂ → α} :
(⨅ (i : ι) (j : ι₂), f i j) = ⨅ (j : ι₂) (i : ι), f i j

theorem supr_comm {α : Type u_1} {ι : Sort u_4} {ι₂ : Sort u_5} [complete_lattice α] {f : ι → ι₂ → α} :
(⨆ (i : ι) (j : ι₂), f i j) = ⨆ (j : ι₂) (i : ι), f i j

@[simp]
theorem infi_infi_eq_left {α : Type u_1} {β : Type u_2} [complete_lattice α] {b : β} {f : Π (x : β), x = b → α} :
(⨅ (x : β) (h : x = b), f x h) = f b rfl

@[simp]
theorem infi_infi_eq_right {α : Type u_1} {β : Type u_2} [complete_lattice α] {b : β} {f : Π (x : β), b = x → α} :
(⨅ (x : β) (h : b = x), f x h) = f b rfl

@[simp]
theorem supr_supr_eq_left {α : Type u_1} {β : Type u_2} [complete_lattice α] {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} [complete_lattice α] {b : β} {f : Π (x : β), b = x → α} :
(⨆ (x : β) (h : b = x), f x h) = f b rfl

theorem infi_subtype {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {p : ι → Prop} {f : subtype p → α} :
(⨅ (x : subtype p), f x) = ⨅ (i : ι) (h : p i), f i, h⟩

theorem infi_subtype' {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {p : ι → Prop} {f : Π (i : ι), p i → α} :
(⨅ (i : ι) (h : p i), f i h) = ⨅ (x : subtype p), f x _

theorem infi_subtype'' {α : Type u_1} [complete_lattice α] {ι : Type u_2} (s : set ι) (f : ι → α) :
(⨅ (i : s), f i) = ⨅ (t : ι) (H : t s), f t

theorem infi_inf_eq {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {f g : ι → α} :
(⨅ (x : ι), f x g x) = (⨅ (x : ι), f x) ⨅ (x : ι), g x

theorem infi_inf {α : Type u_1} {ι : Sort u_4} [complete_lattice α] [h : nonempty ι] {f : ι → α} {a : α} :
(⨅ (x : ι), f x) a = ⨅ (x : ι), f x a

theorem inf_infi {α : Type u_1} {ι : Sort u_4} [complete_lattice α] [nonempty ι] {f : ι → α} {a : α} :
(a ⨅ (x : ι), f x) = ⨅ (x : ι), a f x

theorem binfi_inf {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {p : ι → Prop} {f : Π (i : ι), p i → α} {a : α} :
(∃ (i : ι), p i)((⨅ (i : ι) (h : p i), f i h) a = ⨅ (i : ι) (h : p i), f i h a)

theorem supr_sup_eq {α : Type u_1} {β : Type u_2} [complete_lattice α] {f g : β → α} :
(⨆ (x : β), f x g x) = (⨆ (x : β), f x) ⨆ (x : β), g x

@[simp]
theorem infi_false {α : Type u_1} [complete_lattice α] {s : false → α} :

@[simp]
theorem supr_false {α : Type u_1} [complete_lattice α] {s : false → α} :

@[simp]
theorem infi_true {α : Type u_1} [complete_lattice α] {s : true → α} :

@[simp]
theorem supr_true {α : Type u_1} [complete_lattice α] {s : true → α} :

@[simp]
theorem infi_exists {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {p : ι → Prop} {f : Exists p → α} :
(⨅ (x : Exists p), f x) = ⨅ (i : ι) (h : p i), f _

@[simp]
theorem supr_exists {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {p : ι → Prop} {f : Exists p → α} :
(⨆ (x : Exists p), f x) = ⨆ (i : ι) (h : p i), f _

theorem infi_and {α : Type u_1} [complete_lattice α] {p q : Prop} {s : p q → α} :
infi s = ⨅ (h₁ : p) (h₂ : q), s _

theorem infi_and' {α : Type u_1} [complete_lattice α] {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_and {α : Type u_1} [complete_lattice α] {p q : Prop} {s : p q → α} :
supr s = ⨆ (h₁ : p) (h₂ : q), s _

theorem supr_and' {α : Type u_1} [complete_lattice α] {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_or {α : Type u_1} [complete_lattice α] {p q : Prop} {s : p q → α} :
infi s = (⨅ (h : p), s _) ⨅ (h : q), s _

theorem supr_or {α : Type u_1} [complete_lattice α] {p q : Prop} {s : p q → α} :
(⨆ (x : p q), s x) = (⨆ (i : p), s _) ⨆ (j : q), s _

theorem Sup_range {ι : Sort u_4} {α : Type u_1} [has_Sup α] {f : ι → α} :

theorem Inf_range {ι : Sort u_4} {α : Type u_1} [has_Inf α] {f : ι → α} :

theorem supr_range {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [complete_lattice α] {g : β → α} {f : ι → β} :
(⨆ (b : β) (H : b set.range f), g b) = ⨆ (i : ι), g (f i)

theorem infi_range {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [complete_lattice α] {g : β → α} {f : ι → β} :
(⨅ (b : β) (H : b set.range f), g b) = ⨅ (i : ι), g (f i)

theorem Inf_image {α : Type u_1} {β : Type u_2} [complete_lattice α] {s : set β} {f : β → α} :
Inf (f '' s) = ⨅ (a : β) (H : a s), f a

theorem Sup_image {α : Type u_1} {β : Type u_2} [complete_lattice α] {s : set β} {f : β → α} :
Sup (f '' s) = ⨆ (a : β) (H : a s), f a

theorem infi_emptyset {α : Type u_1} {β : Type u_2} [complete_lattice α] {f : β → α} :
(⨅ (x : β) (H : x ), f x) =

theorem supr_emptyset {α : Type u_1} {β : Type u_2} [complete_lattice α] {f : β → α} :
(⨆ (x : β) (H : x ), f x) =

theorem infi_univ {α : Type u_1} {β : Type u_2} [complete_lattice α] {f : β → α} :
(⨅ (x : β) (H : x set.univ), f x) = ⨅ (x : β), f x

theorem supr_univ {α : Type u_1} {β : Type u_2} [complete_lattice α] {f : β → α} :
(⨆ (x : β) (H : x set.univ), f x) = ⨆ (x : β), f x

theorem infi_union {α : Type u_1} {β : Type u_2} [complete_lattice α] {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_split {α : Type u_1} {β : Type u_2} [complete_lattice α] (f : β → α) (p : β → Prop) :
(⨅ (i : β), f i) = (⨅ (i : β) (h : p i), f i) ⨅ (i : β) (h : ¬p i), f i

theorem infi_split_single {α : Type u_1} {β : Type u_2} [complete_lattice α] (f : β → α) (i₀ : β) :
(⨅ (i : β), f i) = f i₀ ⨅ (i : β) (h : i i₀), f i

theorem infi_le_infi_of_subset {α : Type u_1} {β : Type u_2} [complete_lattice α] {f : β → α} {s t : set β} :
s t((⨅ (x : β) (H : x t), f x) ⨅ (x : β) (H : x s), f x)

theorem supr_union {α : Type u_1} {β : Type u_2} [complete_lattice α] {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} [complete_lattice α] (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} [complete_lattice α] (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} [complete_lattice α] {f : β → α} {s t : set β} :
s t((⨆ (x : β) (H : x s), f x) ⨆ (x : β) (H : x t), f x)

theorem infi_insert {α : Type u_1} {β : Type u_2} [complete_lattice α] {f : β → α} {s : set β} {b : β} :
(⨅ (x : β) (H : x insert b s), f x) = f b ⨅ (x : β) (H : x s), f x

theorem supr_insert {α : Type u_1} {β : Type u_2} [complete_lattice α] {f : β → α} {s : set β} {b : β} :
(⨆ (x : β) (H : x insert b s), f x) = f b ⨆ (x : β) (H : x s), f x

theorem infi_singleton {α : Type u_1} {β : Type u_2} [complete_lattice α] {f : β → α} {b : β} :
(⨅ (x : β) (H : x {b}), f x) = f b

theorem infi_pair {α : Type u_1} {β : Type u_2} [complete_lattice α] {f : β → α} {a b : β} :
(⨅ (x : β) (H : x {a, b}), f x) = f a f b

theorem supr_singleton {α : Type u_1} {β : Type u_2} [complete_lattice α] {f : β → α} {b : β} :
(⨆ (x : β) (H : x {b}), f x) = f b

theorem supr_pair {α : Type u_1} {β : Type u_2} [complete_lattice α] {f : β → α} {a b : β} :
(⨆ (x : β) (H : x {a, b}), f x) = f a f b

theorem infi_image {α : Type u_1} {β : Type u_2} [complete_lattice α] {γ : Type u_3} {f : β → γ} {g : γ → α} {t : set β} :
(⨅ (c : γ) (H : c f '' t), g c) = ⨅ (b : β) (H : b t), g (f b)

theorem supr_image {α : Type u_1} {β : Type u_2} [complete_lattice α] {γ : Type u_3} {f : β → γ} {g : γ → α} {t : set β} :
(⨆ (c : γ) (H : c f '' t), g c) = ⨆ (b : β) (H : b t), g (f b)

supr and infi under Type

theorem infi_of_empty' {α : Type u_1} {ι : Sort u_4} [complete_lattice α] (h : ι → false) {s : ι → α} :

theorem supr_of_empty' {α : Type u_1} {ι : Sort u_4} [complete_lattice α] (h : ι → false) {s : ι → α} :

theorem infi_of_empty {α : Type u_1} {ι : Sort u_4} [complete_lattice α] (h : ¬nonempty ι) {s : ι → α} :

theorem supr_of_empty {α : Type u_1} {ι : Sort u_4} [complete_lattice α] (h : ¬nonempty ι) {s : ι → α} :

@[simp]
theorem infi_empty {α : Type u_1} [complete_lattice α] {s : empty → α} :

@[simp]
theorem supr_empty {α : Type u_1} [complete_lattice α] {s : empty → α} :

@[simp]
theorem infi_unit {α : Type u_1} [complete_lattice α] {f : unit → α} :
(⨅ (x : unit), f x) = f ()

@[simp]
theorem supr_unit {α : Type u_1} [complete_lattice α] {f : unit → α} :
(⨆ (x : unit), f x) = f ()

theorem supr_bool_eq {α : Type u_1} [complete_lattice α] {f : bool → α} :
(⨆ (b : bool), f b) = f tt f ff

theorem infi_bool_eq {α : Type u_1} [complete_lattice α] {f : bool → α} :
(⨅ (b : bool), f b) = f tt f ff

theorem is_glb_binfi {α : Type u_1} {β : Type u_2} [complete_lattice α] {s : set β} {f : β → α} :
is_glb (f '' s) (⨅ (x : β) (H : x s), f x)

theorem supr_subtype {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {p : ι → Prop} {f : subtype p → α} :
(⨆ (x : subtype p), f x) = ⨆ (i : ι) (h : p i), f i, h⟩

theorem supr_subtype' {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {p : ι → Prop} {f : Π (i : ι), p i → α} :
(⨆ (i : ι) (h : p i), f i h) = ⨆ (x : subtype p), f x _

theorem Sup_eq_supr' {α : Type u_1} [complete_lattice α] {s : set α} :
Sup s = ⨆ (x : s), x

theorem is_lub_bsupr {α : Type u_1} {β : Type u_2} [complete_lattice α] {s : set β} {f : β → α} :
is_lub (f '' s) (⨆ (x : β) (H : x s), f x)

theorem infi_sigma {α : Type u_1} {β : Type u_2} [complete_lattice α] {p : β → Type u_3} {f : sigma p → α} :
(⨅ (x : sigma p), f x) = ⨅ (i : β) (h : p i), f i, h⟩

theorem supr_sigma {α : Type u_1} {β : Type u_2} [complete_lattice α] {p : β → Type u_3} {f : sigma p → α} :
(⨆ (x : sigma p), f x) = ⨆ (i : β) (h : p i), f i, h⟩

theorem infi_prod {α : Type u_1} {β : Type u_2} [complete_lattice α] {γ : Type u_3} {f : β × γ → α} :
(⨅ (x : β × γ), f x) = ⨅ (i : β) (j : γ), f (i, j)

theorem supr_prod {α : Type u_1} {β : Type u_2} [complete_lattice α] {γ : Type u_3} {f : β × γ → α} :
(⨆ (x : β × γ), f x) = ⨆ (i : β) (j : γ), f (i, j)

theorem infi_sum {α : Type u_1} {β : Type u_2} [complete_lattice α] {γ : Type u_3} {f : β γ → α} :
(⨅ (x : β γ), f x) = (⨅ (i : β), f (sum.inl i)) ⨅ (j : γ), f (sum.inr j)

theorem supr_sum {α : Type u_1} {β : Type u_2} [complete_lattice α] {γ : Type u_3} {f : β γ → α} :
(⨆ (x : β γ), f x) = (⨆ (i : β), f (sum.inl i)) ⨆ (j : γ), f (sum.inr j)

supr and infi under

theorem supr_ge_eq_supr_nat_add {α : Type u_1} [complete_lattice α] {u : → α} (n : ) :
(⨆ (i : ) (H : i n), u i) = ⨆ (i : ), u (i + n)

theorem infi_ge_eq_infi_nat_add {α : Type u_1} [complete_lattice α] {u : → α} (n : ) :
(⨅ (i : ) (H : i n), u i) = ⨅ (i : ), u (i + n)

theorem supr_eq_top {α : Type u_1} {ι : Sort u_4} [complete_linear_order α] (f : ι → α) :
supr f = ∀ (b : α), b < (∃ (i : ι), b < f i)

theorem infi_eq_bot {α : Type u_1} {ι : Sort u_4} [complete_linear_order α] (f : ι → α) :
infi f = ∀ (b : α), b > (∃ (i : ι), f i < b)

Instances

@[instance]

Equations
theorem Inf_Prop_eq {s : set Prop} :
Inf s = ∀ (p : Prop), p s → p

theorem Sup_Prop_eq {s : set Prop} :
Sup s = ∃ (p : Prop) (H : p s), p

theorem infi_Prop_eq {ι : Sort u_1} {p : ι → Prop} :
(⨅ (i : ι), p i) = ∀ (i : ι), p i

theorem supr_Prop_eq {ι : Sort u_1} {p : ι → Prop} :
(⨆ (i : ι), p i) = ∃ (i : ι), p i

@[instance]
def pi.has_Sup {α : Type u_1} {β : α → Type u_2} [Π (i : α), has_Sup (β i)] :
has_Sup (Π (i : α), β i)

Equations
@[instance]
def pi.has_Inf {α : Type u_1} {β : α → Type u_2} [Π (i : α), has_Inf (β i)] :
has_Inf (Π (i : α), β i)

Equations
theorem Inf_apply {α : Type u_1} {β : α → Type u_2} [Π (i : α), has_Inf (β i)] {s : set (Π (a : α), β a)} {a : α} :
Inf s a = ⨅ (f : s), f a

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 Sup_apply {α : Type u_1} {β : α → Type u_2} [Π (i : α), has_Sup (β i)] {s : set (Π (a : α), β a)} {a : α} :
Sup s a = ⨆ (f : s), f a

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

theorem monotone_Sup_of_monotone {α : Type u_1} {β : Type u_2} [preorder α] [complete_lattice β] {s : set (α → β)} :
(∀ (f : α → β), f smonotone f)monotone (Sup s)

theorem monotone_Inf_of_monotone {α : Type u_1} {β : Type u_2} [preorder α] [complete_lattice β] {s : set (α → β)} :
(∀ (f : α → β), f smonotone f)monotone (Inf s)

@[instance]
def prod.has_Inf (α : Type u_1) (β : Type u_2) [has_Inf α] [has_Inf β] :
has_Inf × β)

Equations
@[instance]
def prod.has_Sup (α : Type u_1) (β : Type u_2) [has_Sup α] [has_Sup β] :
has_Sup × β)

Equations