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 "bounded" supremum 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 #

source
@[class]
structure has_Sup (α : Type u_6) :
Type u_6
  • Sup : set α → α

class for the Sup operator

Instances
source
@[class]
structure has_Inf (α : Type u_6) :
Type u_6
  • Inf : set α → α

class for the Inf operator

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

Indexed supremum

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

Indexed infimum

Equations
source
@[protected, instance]
def has_Inf_to_nonempty (α : Type u_1) [has_Inf α] :
nonempty α
source
@[protected, instance]
def has_Sup_to_nonempty (α : Type u_1) [has_Sup α] :
nonempty α
source
@[protected, instance]
def order_dual.has_Sup (α : Type u_1) [has_Inf α] :
has_Sup (order_dual α)
Equations
source
@[protected, instance]
def order_dual.has_Inf (α : Type u_1) [has_Sup α] :
has_Inf (order_dual α)
Equations
source
@[class]
structure complete_semilattice_Sup (α : Type u_6) :
Type u_6

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
source
@[instance]
def complete_semilattice_Sup.to_has_Sup (α : Type u_6) [self : complete_semilattice_Sup α] :
has_Sup α
source
@[instance]
def complete_semilattice_Sup.to_partial_order (α : Type u_6) [self : complete_semilattice_Sup α] :
partial_order α
source
theorem le_Sup {α : Type u_1} [complete_semilattice_Sup α] {s : set α} {a : α} :
a ∈ s → a ≤ Sup s
source
theorem Sup_le {α : Type u_1} [complete_semilattice_Sup α] {s : set α} {a : α} :
(∀ (b : α), b ∈ s → b ≤ a) → Sup s ≤ a
source
theorem is_lub_Sup {α : Type u_1} [complete_semilattice_Sup α] (s : set α) :
is_lub s (Sup s)
source
theorem is_lub.Sup_eq {α : Type u_1} [complete_semilattice_Sup α] {s : set α} {a : α} (h : is_lub s a) :
Sup s = a
source
theorem le_Sup_of_le {α : Type u_1} [complete_semilattice_Sup α] {s : set α} {a b : α} (hb : b ∈ s) (h : a ≤ b) :
a ≤ Sup s
source
theorem Sup_le_Sup {α : Type u_1} [complete_semilattice_Sup α] {s t : set α} (h : s ⊆ t) :
Sup s ≤ Sup t
source
@[simp]
theorem Sup_le_iff {α : Type u_1} [complete_semilattice_Sup α] {s : set α} {a : α} :
Sup s ≤ a ↔ ∀ (b : α), b ∈ s → b ≤ a
source
theorem le_Sup_iff {α : Type u_1} [complete_semilattice_Sup α] {s : set α} {a : α} :
a ≤ Sup s ↔ ∀ (b : α), b ∈ upper_bounds s → a ≤ b
source
theorem Sup_le_Sup_of_forall_exists_le {α : Type u_1} [complete_semilattice_Sup α] {s t : set α} (h : ∀ (x : α), x ∈ s → (∃ (y : α) (H : y ∈ t), x ≤ y)) :
Sup s ≤ Sup t
source
theorem Sup_singleton {α : Type u_1} [complete_semilattice_Sup α] {a : α} :
Sup {a} = a
source
@[instance]
def complete_semilattice_Inf.to_has_Inf (α : Type u_6) [self : complete_semilattice_Inf α] :
has_Inf α
source
@[instance]
def complete_semilattice_Inf.to_partial_order (α : Type u_6) [self : complete_semilattice_Inf α] :
partial_order α
source
@[class]
structure complete_semilattice_Inf (α : Type u_6) :
Type u_6

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
source
theorem Inf_le {α : Type u_1} [complete_semilattice_Inf α] {s : set α} {a : α} :
a ∈ s → Inf s ≤ a
source
theorem le_Inf {α : Type u_1} [complete_semilattice_Inf α] {s : set α} {a : α} :
(∀ (b : α), b ∈ s → a ≤ b) → a ≤ Inf s
source
theorem is_glb_Inf {α : Type u_1} [complete_semilattice_Inf α] (s : set α) :
is_glb s (Inf s)
source
theorem is_glb.Inf_eq {α : Type u_1} [complete_semilattice_Inf α] {s : set α} {a : α} (h : is_glb s a) :
Inf s = a
source
theorem Inf_le_of_le {α : Type u_1} [complete_semilattice_Inf α] {s : set α} {a b : α} (hb : b ∈ s) (h : b ≤ a) :
Inf s ≤ a
source
theorem Inf_le_Inf {α : Type u_1} [complete_semilattice_Inf α] {s t : set α} (h : s ⊆ t) :
Inf t ≤ Inf s
source
@[simp]
theorem le_Inf_iff {α : Type u_1} [complete_semilattice_Inf α] {s : set α} {a : α} :
a ≤ Inf s ↔ ∀ (b : α), b ∈ s → a ≤ b
source
theorem Inf_le_iff {α : Type u_1} [complete_semilattice_Inf α] {s : set α} {a : α} :
Inf s ≤ a ↔ ∀ (b : α), (∀ (x : α), x ∈ s → b ≤ x) → b ≤ a
source
theorem Inf_le_Inf_of_forall_exists_le {α : Type u_1} [complete_semilattice_Inf α] {s t : set α} (h : ∀ (x : α), x ∈ s → (∃ (y : α) (H : y ∈ t), y ≤ x)) :
Inf t ≤ Inf s
source
theorem Inf_singleton {α : Type u_1} [complete_semilattice_Inf α] {a : α} :
Inf {a} = a
source
@[class]
structure complete_lattice (α : Type u_6) :
Type u_6
  • sup : α → α → α
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a ≤ a
  • le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
  • lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
  • le_sup_left : ∀ (a b : α), a ≤ a ⊔ b
  • le_sup_right : ∀ (a b : α), b ≤ a ⊔ b
  • sup_le : ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ b ≤ c
  • inf : α → α → α
  • inf_le_left : ∀ (a b : α), a ⊓ b ≤ a
  • inf_le_right : ∀ (a b : α), a ⊓ b ≤ b
  • le_inf : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c
  • Sup : set α → α
  • le_Sup : ∀ (s : set α) (a : α), a ∈ s → a ≤ complete_lattice.Sup s
  • Sup_le : ∀ (s : set α) (a : α), (∀ (b : α), b ∈ s → b ≤ a) → complete_lattice.Sup s ≤ a
  • Inf : set α → α
  • Inf_le : ∀ (s : set α) (a : α), a ∈ s → complete_lattice.Inf s ≤ a
  • le_Inf : ∀ (s : set α) (a : α), (∀ (b : α), b ∈ s → a ≤ b) → a ≤ complete_lattice.Inf s
  • top : α
  • bot : α
  • le_top : ∀ (x : α), x ≤ ⊤
  • bot_le : ∀ (x : α), ⊥ ≤ x

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

Instances
source
@[instance]
def complete_lattice.to_lattice (α : Type u_6) [self : complete_lattice α] :
lattice α
source
@[instance]
def complete_lattice.to_complete_semilattice_Sup (α : Type u_6) [self : complete_lattice α] :
complete_semilattice_Sup α
source
@[instance]
def complete_lattice.to_has_top (α : Type u_6) [self : complete_lattice α] :
has_top α
source
@[instance]
def complete_lattice.to_complete_semilattice_Inf (α : Type u_6) [self : complete_lattice α] :
complete_semilattice_Inf α
source
@[instance]
def complete_lattice.to_has_bot (α : Type u_6) [self : complete_lattice α] :
has_bot α
source
@[protected, instance]
def complete_lattice.to_bounded_order {α : Type u_1} [h : complete_lattice α] :
bounded_order α
Equations
source
def complete_lattice_of_Inf (α : Type u_1) [H1 : partial_order α] [H2 : has_Inf α] (is_glb_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. 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
source
def complete_lattice_of_complete_semilattice_Inf (α : Type u_1) [complete_semilattice_Inf α] :
complete_lattice α

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
source
def complete_lattice_of_Sup (α : Type u_1) [H1 : partial_order α] [H2 : has_Sup α] (is_lub_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. 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
source
def complete_lattice_of_complete_semilattice_Sup (α : Type u_1) [complete_semilattice_Sup α] :
complete_lattice α

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
source
@[class]
structure complete_linear_order (α : Type u_6) :
Type u_6

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

Instances
source
@[instance]
def complete_linear_order.to_linear_order (α : Type u_6) [self : complete_linear_order α] :
linear_order α
source
@[instance]
def complete_linear_order.to_complete_lattice (α : Type u_6) [self : complete_linear_order α] :
complete_lattice α
source
@[protected, instance]
def order_dual.complete_lattice (α : Type u_1) [complete_lattice α] :
complete_lattice (order_dual α)
Equations
source
@[protected, instance]
def order_dual.complete_linear_order (α : Type u_1) [complete_linear_order α] :
complete_linear_order (order_dual α)
Equations
source
theorem Inf_le_Sup {α : Type u_1} [complete_lattice α] {s : set α} (hs : s.nonempty) :
Inf s ≤ Sup s
source
theorem Sup_union {α : Type u_1} [complete_lattice α] {s t : set α} :
Sup (s ∪ t) = Sup s ⊔ Sup t
source
theorem Sup_inter_le {α : Type u_1} [complete_lattice α] {s t : set α} :
Sup (s ∩ t) ≤ Sup s ⊓ Sup t
source
theorem Inf_union {α : Type u_1} [complete_lattice α] {s t : set α} :
Inf (s ∪ t) = Inf s ⊓ Inf t
source
theorem le_Inf_inter {α : Type u_1} [complete_lattice α] {s t : set α} :
Inf s ⊔ Inf t ≤ Inf (s ∩ t)
source
@[simp]
theorem Sup_empty {α : Type u_1} [complete_lattice α] :
Sup ∅ = ⊥
source
@[simp]
theorem Inf_empty {α : Type u_1} [complete_lattice α] :
Inf ∅ = ⊤
source
@[simp]
theorem Sup_univ {α : Type u_1} [complete_lattice α] :
Sup set.univ = ⊤
source
@[simp]
theorem Inf_univ {α : Type u_1} [complete_lattice α] :
Inf set.univ = ⊥
source
@[simp]
theorem Sup_insert {α : Type u_1} [complete_lattice α] {a : α} {s : set α} :
Sup (insert a s) = a ⊔ Sup s
source
@[simp]
theorem Inf_insert {α : Type u_1} [complete_lattice α] {a : α} {s : set α} :
Inf (insert a s) = a ⊓ Inf s
source
theorem Sup_le_Sup_of_subset_insert_bot {α : Type u_1} [complete_lattice α] {s t : set α} (h : s ⊆ insert ⊥ t) :
Sup s ≤ Sup t
source
theorem Inf_le_Inf_of_subset_insert_top {α : Type u_1} [complete_lattice α] {s t : set α} (h : s ⊆ insert ⊤ t) :
Inf t ≤ Inf s
source
theorem Sup_pair {α : Type u_1} [complete_lattice α] {a b : α} :
Sup {a, b} = a ⊔ b
source
theorem Inf_pair {α : Type u_1} [complete_lattice α] {a b : α} :
Inf {a, b} = a ⊓ b
source
@[simp]
theorem Inf_eq_top {α : Type u_1} [complete_lattice α] {s : set α} :
Inf s = ⊤ ↔ ∀ (a : α), a ∈ s → a = ⊤
source
theorem eq_singleton_top_of_Inf_eq_top_of_nonempty {α : Type u_1} [complete_lattice α] {s : set α} (h_inf : Inf s = ⊤) (hne : s.nonempty) :
s = {⊤}
source
@[simp]
theorem Sup_eq_bot {α : Type u_1} [complete_lattice α] {s : set α} :
Sup s = ⊥ ↔ ∀ (a : α), a ∈ s → a = ⊥
source
theorem eq_singleton_bot_of_Sup_eq_bot_of_nonempty {α : Type u_1} [complete_lattice α] {s : set α} (h_sup : Sup s = ⊥) (hne : s.nonempty) :
s = {⊥}
source
theorem Sup_eq_of_forall_le_of_forall_lt_exists_gt {α : Type u_1} [complete_lattice α] {s : set α} {b : α} (_x : ∀ (a : α), a ∈ s → a ≤ b) (H : ∀ (w : α), w < b → (∃ (a : α) (H : a ∈ s), w < a)) :
Sup s = 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.

source
theorem Inf_eq_of_forall_ge_of_forall_gt_exists_lt {α : Type u_1} [complete_lattice α] {s : set α} {b : α} (_x : ∀ (a : α), a ∈ s → b ≤ a) (H : ∀ (w : α), b < w → (∃ (a : α) (H : a ∈ s), a < w)) :
Inf s = 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.

source
theorem Inf_lt_iff {α : Type u_1} [complete_linear_order α] {s : set α} {b : α} :
Inf s < b ↔ ∃ (a : α) (H : a ∈ s), a < b
source
theorem lt_Sup_iff {α : Type u_1} [complete_linear_order α] {s : set α} {b : α} :
b < Sup s ↔ ∃ (a : α) (H : a ∈ s), b < a
source
theorem Sup_eq_top {α : Type u_1} [complete_linear_order α] {s : set α} :
Sup s = ⊤ ↔ ∀ (b : α), b < ⊤ → (∃ (a : α) (H : a ∈ s), b < a)
source
theorem Inf_eq_bot {α : Type u_1} [complete_linear_order α] {s : set α} :
Inf s = ⊥ ↔ ∀ (b : α), b > ⊥ → (∃ (a : α) (H : a ∈ s), a < b)
source
theorem lt_supr_iff {α : Type u_1} {ι : Sort u_4} [complete_linear_order α] {a : α} {f : ι → α} :
a < supr f ↔ ∃ (i : ι), a < f i
source
theorem infi_lt_iff {α : Type u_1} {ι : Sort u_4} [complete_linear_order α] {a : α} {f : ι → α} :
infi f < a ↔ ∃ (i : ι), f i < a
source
theorem le_supr {α : Type u_1} {ι : Sort u_4} [complete_lattice α] (s : ι → α) (i : ι) :
s i ≤ supr s
source
theorem le_supr' {α : Type u_1} {ι : Sort u_4} [complete_lattice α] (s : ι → α) (i : ι) :
(:s i ≤ supr s:)
source
theorem is_lub_supr {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {s : ι → α} :
is_lub (set.range s) (⨆ (j : ι), s j)
source
theorem is_lub.supr_eq {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {s : ι → α} {a : α} (h : is_lub (set.range s) a) :
(⨆ (j : ι), s j) = a
source
theorem is_glb_infi {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {s : ι → α} :
is_glb (set.range s) (⨅ (j : ι), s j)
source
theorem is_glb.infi_eq {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {s : ι → α} {a : α} (h : is_glb (set.range s) a) :
(⨅ (j : ι), s j) = a
source
theorem le_supr_of_le {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {s : ι → α} {a : α} (i : ι) (h : a ≤ s i) :
a ≤ supr s
source
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
source
theorem le_bsupr_of_le {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {a : α} {p : ι → Prop} {f : Π (i : ι), p i → α} (i : ι) (hi : p i) (h : a ≤ f i hi) :
a ≤ ⨆ (i : ι) (hi : p i), f i hi
source
theorem supr_le {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {s : ι → α} {a : α} (h : ∀ (i : ι), s i ≤ a) :
supr s ≤ a
source
theorem bsupr_le {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {a : α} {p : ι → Prop} {f : Π (i : ι), p i → α} (h : ∀ (i : ι) (hi : p i), f i hi ≤ a) :
(⨆ (i : ι) (hi : p i), f i hi) ≤ a
source
theorem bsupr_le_supr {α : Type u_1} {ι : Sort u_4} [complete_lattice α] (p : ι → Prop) (f : ι → α) :
(⨆ (i : ι) (H : p i), f i) ≤ ⨆ (i : ι), f i
source
theorem supr_le_supr {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {s t : ι → α} (h : ∀ (i : ι), s i ≤ t i) :
supr s ≤ supr t
source
theorem supr_le_supr2 {α : Type u_1} {ι : Sort u_4} {ι₂ : Sort u_5} [complete_lattice α] {s : ι → α} {t : ι₂ → α} (h : ∀ (i : ι), ∃ (j : ι₂), s i ≤ t j) :
supr s ≤ supr t
source
theorem bsupr_le_bsupr {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {p : ι → Prop} {f g : Π (i : ι), p i → α} (h : ∀ (i : ι) (hi : p i), f i hi ≤ g i hi) :
(⨆ (i : ι) (hi : p i), f i hi) ≤ ⨆ (i : ι) (hi : p i), g i hi
source
theorem supr_le_supr_const {α : Type u_1} {ι : Sort u_4} {ι₂ : Sort u_5} [complete_lattice α] {a : α} (h : ι → ι₂) :
(⨆ (i : ι), a) ≤ ⨆ (j : ι₂), a
source
theorem bsupr_le_bsupr' {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {p q : ι → Prop} (hpq : ∀ (i : ι), p i → q i) {f : ι → α} :
(⨆ (i : ι) (hpi : p i), f i) ≤ ⨆ (i : ι) (hqi : q i), f i
source
@[simp]
theorem supr_le_iff {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {s : ι → α} {a : α} :
supr s ≤ a ↔ ∀ (i : ι), s i ≤ a
source
theorem supr_lt_iff {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {s : ι → α} {a : α} :
supr s < a ↔ ∃ (b : α) (H : b < a), ∀ (i : ι), s i ≤ b
source
theorem Sup_eq_supr {α : Type u_1} [complete_lattice α] {s : set α} :
Sup s = ⨆ (a : α) (H : a ∈ s), a
source
theorem Sup_eq_supr' {α : Type u_1} [has_Sup α] (s : set α) :
Sup s = ⨆ (x : ↥s), ↑x
source
theorem Sup_sUnion {α : Type u_1} [complete_lattice α] {s : set (set α)} :
Sup (⋃₀s) = ⨆ (t : set α) (H : t ∈ s), Sup t
source
theorem le_supr_iff {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {s : ι → α} {a : α} :
a ≤ supr s ↔ ∀ (b : α), (∀ (i : ι), s i ≤ b) → a ≤ b
source
theorem monotone.le_map_supr {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [complete_lattice α] {s : ι → α} [complete_lattice β] {f : α → β} (hf : monotone f) :
(⨆ (i : ι), f (s i)) ≤ f (supr s)
source
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)
source
theorem monotone.le_map_Sup {α : Type u_1} {β : Type u_2} [complete_lattice α] [complete_lattice β] {s : set α} {f : α → β} (hf : monotone f) :
(⨆ (a : α) (H : a ∈ s), f a) ≤ f (Sup s)
source
theorem order_iso.map_supr {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [complete_lattice α] [complete_lattice β] (f : α ≃o β) (x : ι → α) :
⇑f (⨆ (i : ι), x i) = ⨆ (i : ι), ⇑f (x i)
source
theorem order_iso.map_Sup {α : Type u_1} {β : Type u_2} [complete_lattice α] [complete_lattice β] (f : α ≃o β) (s : set α) :
⇑f (Sup s) = ⨆ (a : α) (H : a ∈ s), ⇑f a
source
theorem supr_comp_le {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {ι' : Sort u_2} (f : ι' → α) (g : ι → ι') :
(⨆ (x : ι), f (g x)) ≤ ⨆ (y : ι'), f y
source
theorem monotone.supr_comp_eq {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [complete_lattice α] [preorder β] {f : β → α} (hf : monotone f) {s : ι → β} (hs : ∀ (x : β), ∃ (i : ι), x ≤ s i) :
(⨆ (x : ι), f (s x)) = ⨆ (y : β), f y
source
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
source
theorem supr_congr {ι : Sort u_4} {ι₂ : Sort u_5} {α : Type u_1} [has_Sup α] {f : ι → α} {g : ι₂ → α} (h : ι → ι₂) (h1 : function.surjective h) (h2 : ∀ (x : ι), g (h x) = f x) :
(⨆ (x : ι), f x) = ⨆ (y : ι₂), g y
source
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₂
source
theorem infi_le {α : Type u_1} {ι : Sort u_4} [complete_lattice α] (s : ι → α) (i : ι) :
infi s ≤ s i
source
theorem infi_le' {α : Type u_1} {ι : Sort u_4} [complete_lattice α] (s : ι → α) (i : ι) :
(:infi s ≤ s i:)
source
theorem infi_le_of_le {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {s : ι → α} {a : α} (i : ι) (h : s i ≤ a) :
infi s ≤ a
source
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
source
theorem binfi_le_of_le {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {a : α} {p : ι → Prop} {f : Π (i : ι), p i → α} (i : ι) (hi : p i) (h : f i hi ≤ a) :
(⨅ (i : ι) (hi : p i), f i hi) ≤ a
source
theorem le_infi {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {s : ι → α} {a : α} (h : ∀ (i : ι), a ≤ s i) :
a ≤ infi s
source
theorem le_binfi {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {a : α} {p : ι → Prop} {f : Π (i : ι), p i → α} (h : ∀ (i : ι) (hi : p i), a ≤ f i hi) :
a ≤ ⨅ (i : ι) (hi : p i), f i hi
source
theorem infi_le_binfi {α : Type u_1} {ι : Sort u_4} [complete_lattice α] (p : ι → Prop) (f : ι → α) :
(⨅ (i : ι), f i) ≤ ⨅ (i : ι) (H : p i), f i
source
theorem infi_le_infi {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {s t : ι → α} (h : ∀ (i : ι), s i ≤ t i) :
infi s ≤ infi t
source
theorem infi_le_infi2 {α : Type u_1} {ι : Sort u_4} {ι₂ : Sort u_5} [complete_lattice α] {s : ι → α} {t : ι₂ → α} (h : ∀ (j : ι₂), ∃ (i : ι), s i ≤ t j) :
infi s ≤ infi t
source
theorem binfi_le_binfi {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {p : ι → Prop} {f g : Π (i : ι), p i → α} (h : ∀ (i : ι) (hi : p i), f i hi ≤ g i hi) :
(⨅ (i : ι) (hi : p i), f i hi) ≤ ⨅ (i : ι) (hi : p i), g i hi
source
theorem infi_le_infi_const {α : Type u_1} {ι : Sort u_4} {ι₂ : Sort u_5} [complete_lattice α] {a : α} (h : ι₂ → ι) :
(⨅ (i : ι), a) ≤ ⨅ (j : ι₂), a
source
@[simp]
theorem le_infi_iff {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {s : ι → α} {a : α} :
a ≤ infi s ↔ ∀ (i : ι), a ≤ s i
source
theorem Inf_eq_infi {α : Type u_1} [complete_lattice α] {s : set α} :
Inf s = ⨅ (a : α) (H : a ∈ s), a
source
theorem Inf_eq_infi' {α : Type u_1} [has_Inf α] (s : set α) :
Inf s = ⨅ (a : ↥s), ↑a
source
theorem monotone.map_infi_le {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [complete_lattice α] {s : ι → α} [complete_lattice β] {f : α → β} (hf : monotone f) :
f (infi s) ≤ ⨅ (i : ι), f (s i)
source
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)
source
theorem monotone.map_Inf_le {α : Type u_1} {β : Type u_2} [complete_lattice α] [complete_lattice β] {s : set α} {f : α → β} (hf : monotone f) :
f (Inf s) ≤ ⨅ (a : α) (H : a ∈ s), f a
source
theorem order_iso.map_infi {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [complete_lattice α] [complete_lattice β] (f : α ≃o β) (x : ι → α) :
⇑f (⨅ (i : ι), x i) = ⨅ (i : ι), ⇑f (x i)
source
theorem order_iso.map_Inf {α : Type u_1} {β : Type u_2} [complete_lattice α] [complete_lattice β] (f : α ≃o β) (s : set α) :
⇑f (Inf s) = ⨅ (a : α) (H : a ∈ s), ⇑f a
source
theorem le_infi_comp {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {ι' : Sort u_2} (f : ι' → α) (g : ι → ι') :
(⨅ (y : ι'), f y) ≤ ⨅ (x : ι), f (g x)
source
theorem monotone.infi_comp_eq {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [complete_lattice α] [preorder β] {f : β → α} (hf : monotone f) {s : ι → β} (hs : ∀ (x : β), ∃ (i : ι), s i ≤ x) :
(⨅ (x : ι), f (s x)) = ⨅ (y : β), f y
source
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
source
theorem infi_congr {ι : Sort u_4} {ι₂ : Sort u_5} {α : Type u_1} [has_Inf α] {f : ι → α} {g : ι₂ → α} (h : ι → ι₂) (h1 : function.surjective h) (h2 : ∀ (x : ι), g (h x) = f x) :
(⨅ (x : ι), f x) = ⨅ (y : ι₂), g y
source
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₂
source
theorem supr_const_le {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {x : α} :
(⨆ (h : ι), x) ≤ x
source
theorem le_infi_const {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {x : α} :
x ≤ ⨅ (h : ι), x
source
theorem infi_const {α : Type u_1} {ι : Sort u_4} [complete_lattice α] [nonempty ι] {a : α} :
(⨅ (b : ι), a) = a
source
theorem supr_const {α : Type u_1} {ι : Sort u_4} [complete_lattice α] [nonempty ι] {a : α} :
(⨆ (b : ι), a) = a
source
@[simp]
theorem infi_top {α : Type u_1} {ι : Sort u_4} [complete_lattice α] :
(⨅ (i : ι), ⊤) = ⊤
source
@[simp]
theorem supr_bot {α : Type u_1} {ι : Sort u_4} [complete_lattice α] :
(⨆ (i : ι), ⊥) = ⊥
source
@[simp]
theorem infi_eq_top {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {s : ι → α} :
infi s = ⊤ ↔ ∀ (i : ι), s i = ⊤
source
@[simp]
theorem supr_eq_bot {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {s : ι → α} :
supr s = ⊥ ↔ ∀ (i : ι), s i = ⊥
source
@[simp]
theorem infi_pos {α : Type u_1} [complete_lattice α] {p : Prop} {f : p → α} (hp : p) :
(⨅ (h : p), f h) = f hp
source
@[simp]
theorem infi_neg {α : Type u_1} [complete_lattice α] {p : Prop} {f : p → α} (hp : ¬p) :
(⨅ (h : p), f h) = ⊤
source
@[simp]
theorem supr_pos {α : Type u_1} [complete_lattice α] {p : Prop} {f : p → α} (hp : p) :
(⨆ (h : p), f h) = f hp
source
@[simp]
theorem supr_neg {α : Type u_1} [complete_lattice α] {p : Prop} {f : p → α} (hp : ¬p) :
(⨆ (h : p), f h) = ⊥
source
theorem supr_eq_of_forall_le_of_forall_lt_exists_gt {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {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.

source
theorem infi_eq_of_forall_ge_of_forall_gt_exists_lt {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {b : α} {f : ι → α} (h₁ : ∀ (i : ι), b ≤ f i) (h₂ : ∀ (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.

source
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), ⊥)
source
theorem supr_eq_if {α : Type u_1} [complete_lattice α] {p : Prop} [decidable p] (a : α) :
(⨆ (h : p), a) = ite p a ⊥
source
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), ⊤)
source
theorem infi_eq_if {α : Type u_1} [complete_lattice α] {p : Prop} [decidable p] (a : α) :
(⨅ (h : p), a) = ite p a ⊤
source
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
source
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
source
@[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
source
@[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
source
@[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
source
@[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
source
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⟩
source
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 _
source
theorem infi_subtype'' {α : Type u_1} [complete_lattice α] {ι : Type u_2} (s : set ι) (f : ι → α) :
(⨅ (i : ↥s), f ↑i) = ⨅ (t : ι) (H : t ∈ s), f t
source
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
source
theorem infi_inf {α : Type u_1} {ι : Sort u_4} [complete_lattice α] [h : nonempty ι] {f : ι → α} {a : α} :
(⨅ (x : ι), f x) ⊓ a = ⨅ (x : ι), f x ⊓ a
source
theorem inf_infi {α : Type u_1} {ι : Sort u_4} [complete_lattice α] [nonempty ι] {f : ι → α} {a : α} :
(a ⊓ ⨅ (x : ι), f x) = ⨅ (x : ι), a ⊓ f x
source
theorem binfi_inf {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {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
source
theorem inf_binfi {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {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
source
theorem supr_sup_eq {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {f g : ι → α} :
(⨆ (x : ι), f x ⊔ g x) = (⨆ (x : ι), f x) ⊔ ⨆ (x : ι), g x
source
theorem supr_sup {α : Type u_1} {ι : Sort u_4} [complete_lattice α] [h : nonempty ι] {f : ι → α} {a : α} :
(⨆ (x : ι), f x) ⊔ a = ⨆ (x : ι), f x ⊔ a
source
theorem sup_supr {α : Type u_1} {ι : Sort u_4} [complete_lattice α] [nonempty ι] {f : ι → α} {a : α} :
(a ⊔ ⨆ (x : ι), f x) = ⨆ (x : ι), a ⊔ f x

supr and infi under Prop #

source
@[simp]
theorem infi_false {α : Type u_1} [complete_lattice α] {s : false → α} :
infi s = ⊤
source
@[simp]
theorem supr_false {α : Type u_1} [complete_lattice α] {s : false → α} :
supr s = ⊥
source
theorem infi_true {α : Type u_1} [complete_lattice α] {s : true → α} :
infi s = s trivial
source
theorem supr_true {α : Type u_1} [complete_lattice α] {s : true → α} :
supr s = s trivial
source
@[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 _
source
@[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 _
source
theorem infi_and {α : Type u_1} [complete_lattice α] {p q : Prop} {s : p ∧ q → α} :
infi s = ⨅ (h₁ : p) (h₂ : q), s _
source
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

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

source
theorem infi_or {α : Type u_1} [complete_lattice α] {p q : Prop} {s : p ∨ q → α} :
infi s = (⨅ (h : p), s _) ⊓ ⨅ (h : q), s _
source
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 _
source
theorem supr_dite {α : Type u_1} {ι : Sort u_4} [complete_lattice α] (p : ι → Prop) [decidable_pred p] (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
source
theorem supr_ite {α : Type u_1} {ι : Sort u_4} [complete_lattice α] (p : ι → Prop) [decidable_pred p] (f g : ι → α) :
(⨆ (i : ι), ite (p i) (f i) (g i)) = (⨆ (i : ι) (h : p i), f i) ⊔ ⨆ (i : ι) (h : ¬p i), g i
source
theorem infi_dite {α : Type u_1} {ι : Sort u_4} [complete_lattice α] (p : ι → Prop) [decidable_pred p] (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
source
theorem infi_ite {α : Type u_1} {ι : Sort u_4} [complete_lattice α] (p : ι → Prop) [decidable_pred p] (f g : ι → α) :
(⨅ (i : ι), ite (p i) (f i) (g i)) = (⨅ (i : ι) (h : p i), f i) ⊓ ⨅ (i : ι) (h : ¬p i), g i
source
theorem Sup_range {ι : Sort u_4} {α : Type u_1} [has_Sup α] {f : ι → α} :
Sup (set.range f) = supr f
source
theorem Inf_range {ι : Sort u_4} {α : Type u_1} [has_Inf α] {f : ι → α} :
Inf (set.range f) = infi f
source
theorem supr_range' {β : Type u_2} {ι : Sort u_4} {α : Type u_1} [has_Sup α] (g : β → α) (f : ι → β) :
(⨆ (b : ↥(set.range f)), g ↑b) = ⨆ (i : ι), g (f i)
source
theorem infi_range' {β : Type u_2} {ι : Sort u_4} {α : Type u_1} [has_Inf α] (g : β → α) (f : ι → β) :
(⨅ (b : ↥(set.range f)), g ↑b) = ⨅ (i : ι), g (f i)
source
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)
source
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)
source
theorem Inf_image' {β : Type u_2} {α : Type u_1} [has_Inf α] {s : set β} {f : β → α} :
Inf (f '' s) = ⨅ (a : ↥s), f ↑a
source
theorem Sup_image' {β : Type u_2} {α : Type u_1} [has_Sup α] {s : set β} {f : β → α} :
Sup (f '' s) = ⨆ (a : ↥s), f ↑a
source
theorem Inf_image {α : Type u_1} {β : Type u_2} [complete_lattice α] {s : set β} {f : β → α} :
Inf (f '' s) = ⨅ (a : β) (H : a ∈ s), f a
source
theorem Sup_image {α : Type u_1} {β : Type u_2} [complete_lattice α] {s : set β} {f : β → α} :
Sup (f '' s) = ⨆ (a : β) (H : a ∈ s), f a
source
theorem infi_emptyset {α : Type u_1} {β : Type u_2} [complete_lattice α] {f : β → α} :
(⨅ (x : β) (H : x ∈ ∅), f x) = ⊤
source
theorem supr_emptyset {α : Type u_1} {β : Type u_2} [complete_lattice α] {f : β → α} :
(⨆ (x : β) (H : x ∈ ∅), f x) = ⊥
source
theorem infi_univ {α : Type u_1} {β : Type u_2} [complete_lattice α] {f : β → α} :
(⨅ (x : β) (H : x ∈ set.univ), f x) = ⨅ (x : β), f x
source
theorem supr_univ {α : Type u_1} {β : Type u_2} [complete_lattice α] {f : β → α} :
(⨆ (x : β) (H : x ∈ set.univ), f x) = ⨆ (x : β), f x
source
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
source
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
source
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
source
theorem infi_le_infi_of_subset {α : Type u_1} {β : Type u_2} [complete_lattice α] {f : β → α} {s t : set β} (h : s ⊆ t) :
(⨅ (x : β) (H : x ∈ t), f x) ≤ ⨅ (x : β) (H : x ∈ s), f x
source
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
source
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
source
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
source
theorem supr_le_supr_of_subset {α : Type u_1} {β : Type u_2} [complete_lattice α] {f : β → α} {s t : set β} (h : s ⊆ t) :
(⨆ (x : β) (H : x ∈ s), f x) ≤ ⨆ (x : β) (H : x ∈ t), f x
source
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
source
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
source
theorem infi_singleton {α : Type u_1} {β : Type u_2} [complete_lattice α] {f : β → α} {b : β} :
(⨅ (x : β) (H : x ∈ {b}), f x) = f b
source
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
source
theorem supr_singleton {α : Type u_1} {β : Type u_2} [complete_lattice α] {f : β → α} {b : β} :
(⨆ (x : β) (H : x ∈ {b}), f x) = f b
source
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
source
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)
source
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 #

source
theorem supr_of_empty' {α : Type u_1} {ι : Sort u_2} [has_Sup α] [is_empty ι] (f : ι → α) :
supr f = Sup ∅
source
theorem supr_of_empty {α : Type u_1} {ι : Sort u_4} [complete_lattice α] [is_empty ι] (f : ι → α) :
supr f = ⊥
source
theorem infi_of_empty' {α : Type u_1} {ι : Sort u_2} [has_Inf α] [is_empty ι] (f : ι → α) :
infi f = Inf ∅
source
theorem infi_of_empty {α : Type u_1} {ι : Sort u_4} [complete_lattice α] [is_empty ι] (f : ι → α) :
infi f = ⊤
source
theorem supr_bool_eq {α : Type u_1} [complete_lattice α] {f : bool → α} :
(⨆ (b : bool), f b) = f tt ⊔ f ff
source
theorem infi_bool_eq {α : Type u_1} [complete_lattice α] {f : bool → α} :
(⨅ (b : bool), f b) = f tt ⊓ f ff
source
theorem sup_eq_supr {α : Type u_1} [complete_lattice α] (x y : α) :
x ⊔ y = ⨆ (b : bool), cond b x y
source
theorem inf_eq_infi {α : Type u_1} [complete_lattice α] (x y : α) :
x ⊓ y = ⨅ (b : bool), cond b x y
source
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)
source
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⟩
source
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 _
source
theorem supr_subtype'' {α : Type u_1} [complete_lattice α] {ι : Type u_2} (s : set ι) (f : ι → α) :
(⨆ (i : ↥s), f ↑i) = ⨆ (t : ι) (H : t ∈ s), f t
source
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)
source
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⟩
source
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⟩
source
theorem infi_prod {α : Type u_1} {β : Type u_2} [complete_lattice α] {γ : Type u_3} {f : β × γ → α} :
(⨅ (x : β × γ), f x) = ⨅ (i : β) (j : γ), f (i, j)
source
theorem supr_prod {α : Type u_1} {β : Type u_2} [complete_lattice α] {γ : Type u_3} {f : β × γ → α} :
(⨆ (x : β × γ), f x) = ⨆ (i : β) (j : γ), f (i, j)
source
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)
source
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)
source
theorem supr_option {α : Type u_1} {β : Type u_2} [complete_lattice α] (f : option β → α) :
(⨆ (o : option β), f o) = f none ⊔ ⨆ (b : β), f (some b)
source
theorem infi_option {α : Type u_1} {β : Type u_2} [complete_lattice α] (f : option β → α) :
(⨅ (o : option β), f o) = f none ⊓ ⨅ (b : β), f (some b)
source
theorem supr_option_elim {α : Type u_1} {β : Type u_2} [complete_lattice α] (a : α) (f : β → α) :
(⨆ (o : option β), o.elim a f) = a ⊔ ⨆ (b : β), f b

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

source
theorem infi_option_elim {α : Type u_1} {β : Type u_2} [complete_lattice α] (a : α) (f : β → α) :
(⨅ (o : option β), o.elim a f) = a ⊓ ⨅ (b : β), f b

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

source
theorem supr_ne_bot_subtype {α : Type u_1} {ι : Sort u_4} [complete_lattice α] (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.

source
theorem infi_ne_top_subtype {α : Type u_1} {ι : Sort u_4} [complete_lattice α] (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.

supr and infi under ℕ #

source
theorem supr_ge_eq_supr_nat_add {α : Type u_1} [complete_lattice α] {u : ℕ → α} (n : ℕ) :
(⨆ (i : ℕ) (H : i ≥ n), u i) = ⨆ (i : ℕ), u (i + n)
source
theorem infi_ge_eq_infi_nat_add {α : Type u_1} [complete_lattice α] {u : ℕ → α} (n : ℕ) :
(⨅ (i : ℕ) (H : i ≥ n), u i) = ⨅ (i : ℕ), u (i + n)
source
theorem monotone.supr_nat_add {α : Type u_1} [complete_lattice α] {f : ℕ → α} (hf : monotone f) (k : ℕ) :
(⨆ (n : ℕ), f (n + k)) = ⨆ (n : ℕ), f n
source
@[simp]
theorem supr_infi_ge_nat_add {α : Type u_1} [complete_lattice α] (f : ℕ → α) (k : ℕ) :
(⨆ (n : ℕ), ⨅ (i : ℕ) (H : i ≥ n), f (i + k)) = ⨆ (n : ℕ), ⨅ (i : ℕ) (H : i ≥ n), f i
source
theorem sup_supr_nat_succ {α : Type u_1} [complete_lattice α] (u : ℕ → α) :
(u 0 ⊔ ⨆ (i : ℕ), u (i + 1)) = ⨆ (i : ℕ), u i
source
theorem inf_infi_nat_succ {α : Type u_1} [complete_lattice α] (u : ℕ → α) :
(u 0 ⊓ ⨅ (i : ℕ), u (i + 1)) = ⨅ (i : ℕ), u i
source
theorem supr_eq_top {α : Type u_1} {ι : Sort u_4} [complete_linear_order α] (f : ι → α) :
supr f = ⊤ ↔ ∀ (b : α), b < ⊤ → (∃ (i : ι), b < f i)
source
theorem infi_eq_bot {α : Type u_1} {ι : Sort u_4} [complete_linear_order α] (f : ι → α) :
infi f = ⊥ ↔ ∀ (b : α), b > ⊥ → (∃ (i : ι), f i < b)

Instances #

source
@[protected, instance]
def Prop.complete_lattice  :
complete_lattice Prop
Equations
source
@[simp]
theorem Inf_Prop_eq {s : set Prop} :
Inf s = ∀ (p : Prop), p ∈ s → p
source
@[simp]
theorem Sup_Prop_eq {s : set Prop} :
Sup s = ∃ (p : Prop) (H : p ∈ s), p
source
@[simp]
theorem infi_Prop_eq {ι : Sort u_1} {p : ι → Prop} :
(⨅ (i : ι), p i) = ∀ (i : ι), p i
source
@[simp]
theorem supr_Prop_eq {ι : Sort u_1} {p : ι → Prop} :
(⨆ (i : ι), p i) = ∃ (i : ι), p i
source
@[protected, instance]
def pi.has_Sup {α : Type u_1} {β : α → Type u_2} [Π (i : α), has_Sup (β i)] :
has_Sup (Π (i : α), β i)
Equations
source
@[protected, instance]
def pi.has_Inf {α : Type u_1} {β : α → Type u_2} [Π (i : α), has_Inf (β i)] :
has_Inf (Π (i : α), β i)
Equations
source
@[protected, instance]
def pi.complete_lattice {α : Type u_1} {β : α → Type u_2} [Π (i : α), complete_lattice (β i)] :
complete_lattice (Π (i : α), β i)
Equations
source
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
source
@[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
source
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
source
theorem unary_relation_Sup_iff {α : Type u_1} (s : set (α → Prop)) {a : α} :
Sup s a ↔ ∃ (r : α → Prop), r ∈ s ∧ r a
source
theorem binary_relation_Sup_iff {α : Type u_1} {β : Type u_2} (s : set (α → β → Prop)) {a : α} {b : β} :
Sup s a b ↔ ∃ (r : α → β → Prop), r ∈ s ∧ r a b
source
@[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
source
theorem monotone_Sup_of_monotone {α : Type u_1} {β : Type u_2} [preorder α] [complete_lattice β] {s : set (α → β)} (m_s : ∀ (f : α → β), f ∈ s → monotone f) :
monotone (Sup s)
source
theorem monotone_Inf_of_monotone {α : Type u_1} {β : Type u_2} [preorder α] [complete_lattice β] {s : set (α → β)} (m_s : ∀ (f : α → β), f ∈ s → monotone f) :
monotone (Inf s)
source
@[protected, instance]
def prod.has_Inf (α : Type u_1) (β : Type u_2) [has_Inf α] [has_Inf β] :
has_Inf (α × β)
Equations
source
@[protected, instance]
def prod.has_Sup (α : Type u_1) (β : Type u_2) [has_Sup α] [has_Sup β] :
has_Sup (α × β)
Equations
source
@[protected, instance]
def prod.complete_lattice (α : Type u_1) (β : Type u_2) [complete_lattice α] [complete_lattice β] :
complete_lattice (α × β)
Equations
source
theorem sup_Inf_le_infi_sup {α : Type u_1} [complete_lattice α] {a : α} {s : set α} :
a ⊔ Inf s ≤ ⨅ (b : α) (H : b ∈ s), a ⊔ b

This is a weaker version of sup_Inf_eq

source
theorem Inf_sup_le_infi_sup {α : Type u_1} [complete_lattice α] {a : α} {s : set α} :
Inf s ⊔ a ≤ ⨅ (b : α) (H : b ∈ s), b ⊔ a

This is a weaker version of Inf_sup_eq

source
theorem supr_inf_le_inf_Sup {α : Type u_1} [complete_lattice α] {a : α} {s : set α} :
(⨆ (b : α) (H : b ∈ s), a ⊓ b) ≤ a ⊓ Sup s

This is a weaker version of inf_Sup_eq

source
theorem supr_inf_le_Sup_inf {α : Type u_1} [complete_lattice α] {a : α} {s : set α} :
(⨆ (b : α) (H : b ∈ s), b ⊓ a) ≤ Sup s ⊓ a

This is a weaker version of Sup_inf_eq

source
theorem disjoint_Sup_left {α : Type u_1} [complete_lattice α] {a : set α} {b : α} (d : disjoint (Sup a) b) {i : α} (hi : i ∈ a) :
disjoint i b
source
theorem disjoint_Sup_right {α : Type u_1} [complete_lattice α] {a : set α} {b : α} (d : disjoint b (Sup a)) {i : α} (hi : i ∈ a) :
disjoint b i
source
def complete_lattice.set_independent {α : Type u_1} [complete_lattice α] (s : set α) :
Prop

An independent set of elements in a complete lattice is one in which every element is disjoint from the Sup of the rest.

Equations
source
@[simp]
theorem complete_lattice.set_independent_empty {α : Type u_1} [complete_lattice α] :
complete_lattice.set_independent ∅
source
theorem complete_lattice.set_independent.mono {α : Type u_1} [complete_lattice α] {s : set α} (hs : complete_lattice.set_independent s) {t : set α} (hst : t ⊆ s) :
complete_lattice.set_independent t
source
theorem complete_lattice.set_independent.disjoint {α : Type u_1} [complete_lattice α] {s : set α} (hs : complete_lattice.set_independent s) {x y : α} (hx : x ∈ s) (hy : y ∈ s) (h : x ≠ y) :
disjoint x y

If the elements of a set are independent, then any pair within that set is disjoint.

source
theorem complete_lattice.set_independent.disjoint_Sup {α : Type u_1} [complete_lattice α] {s : set α} (hs : complete_lattice.set_independent s) {x : α} {y : set α} (hx : x ∈ s) (hy : y ⊆ s) (hxy : x ∉ y) :
disjoint x (Sup y)

If the elements of a set are independent, then any element is disjoint from the Sup of some subset of the rest.

source
def complete_lattice.independent {ι : Sort u_1} {α : Type u_2} [complete_lattice α] (t : ι → α) :
Prop

An independent indexed family of elements in a complete lattice is one in which every element is disjoint from the supr of the rest.

Example: an indexed family of non-zero elements in a vector space is linearly independent iff the indexed family of subspaces they generate is independent in this sense.

Example: an indexed family of submodules of a module is independent in this sense if and only the natural map from the direct sum of the submodules to the module is injective.

Equations
source
theorem complete_lattice.set_independent_iff {α : Type u_1} [complete_lattice α] (s : set α) :
complete_lattice.set_independent s ↔ complete_lattice.independent coe
source
theorem complete_lattice.independent_def {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {t : ι → α} :
complete_lattice.independent t ↔ ∀ (i : ι), disjoint (t i) (⨆ (j : ι) (H : j ≠ i), t j)
source
theorem complete_lattice.independent_def' {α : Type u_1} [complete_lattice α] {ι : Type u_2} {t : ι → α} :
complete_lattice.independent t ↔ ∀ (i : ι), disjoint (t i) (Sup (t '' {j : ι | j ≠ i}))
source
theorem complete_lattice.independent_def'' {α : Type u_1} [complete_lattice α] {ι : Type u_2} {t : ι → α} :
complete_lattice.independent t ↔ ∀ (i : ι), disjoint (t i) (Sup {a : α | ∃ (j : ι) (H : j ≠ i), t j = a})
source
@[simp]
theorem complete_lattice.independent_empty {α : Type u_1} [complete_lattice α] (t : empty → α) :
complete_lattice.independent t
source
@[simp]
theorem complete_lattice.independent_pempty {α : Type u_1} [complete_lattice α] (t : pempty → α) :
complete_lattice.independent t
source
theorem complete_lattice.independent.disjoint {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {t : ι → α} (ht : complete_lattice.independent t) {x y : ι} (h : x ≠ y) :
disjoint (t x) (t y)

If the elements of a set are independent, then any pair within that set is disjoint.

source
theorem complete_lattice.independent.mono {ι : Type u_1} {α : Type u_2} [complete_lattice α] {s t : ι → α} (hs : complete_lattice.independent s) (hst : t ≤ s) :
complete_lattice.independent t
source
theorem complete_lattice.independent.comp {ι : Sort u_1} {ι' : Sort u_2} {α : Type u_3} [complete_lattice α] {s : ι → α} (hs : complete_lattice.independent s) (f : ι' → ι) (hf : function.injective f) :
complete_lattice.independent (s ∘ f)

Composing an independent indexed family with an injective function on the index results in another indepedendent indexed family.

source
theorem complete_lattice.independent.map_order_iso {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [complete_lattice α] [complete_lattice β] (f : α ≃o β) {a : ι → α} (ha : complete_lattice.independent a) :
complete_lattice.independent (⇑f ∘ a)

Composing an indepedent indexed family with an order isomorphism on the elements results in another indepedendent indexed family.

source
@[simp]
theorem complete_lattice.independent_map_order_iso_iff {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [complete_lattice α] [complete_lattice β] (f : α ≃o β) {a : ι → α} :
complete_lattice.independent (⇑f ∘ a) ↔ complete_lattice.independent a
source
theorem complete_lattice.independent.disjoint_bsupr {ι : Type u_1} {α : Type u_2} [complete_lattice α] {t : ι → α} (ht : complete_lattice.independent t) {x : ι} {y : set ι} (hx : x ∉ y) :
disjoint (t x) (⨆ (i : ι) (H : i ∈ y), t i)

If the elements of a set are independent, then any element is disjoint from the supr of some subset of the rest.