mathlib docs: order.complete

sup : α → α → α
le : α → α → Prop
lt : α → α → Prop
le_refl : ∀ (a : α), a ≤ a
le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
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_1 : α), a ≤ c_1 → b ≤ c_1 → a ⊔ 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 ≤ b → a ≤ c_1 → a ≤ b ⊓ c_1
top : α
le_top : ∀ (a : α), a ≤ ⊤
bot : α
bot_le : ∀ (a : α), ⊥ ≤ a
Sup : set α → α
Inf : 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_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

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

Instances

source

@[instance]

def complete_lattice.to_bounded_lattice (α : Type u_6) [s : complete_lattice α] :

bounded_lattice α

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

Equations

complete_lattice_of_Inf α is_glb_Inf = {sup := λ (a b : α), Inf {x : α | a ≤ x ∧ b ≤ x}, le := partial_order.le H1, lt := partial_order.lt H1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := λ (a b : α), Inf {a, b}, inf_le_left := _, inf_le_right := _, le_inf := _, top := Inf ∅, le_top := _, bot := Inf set.univ, bot_le := _, Sup := λ (s : set α), Inf (upper_bounds s), Inf := Inf H2, le_Sup := _, Sup_le := _, Inf_le := _, le_Inf := _}

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

Equations

complete_lattice_of_Sup α is_lub_Sup = {sup := λ (a b : α), Sup {a, b}, le := partial_order.le H1, lt := partial_order.lt H1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := λ (a b : α), Sup {x : α | x ≤ a ∧ x ≤ b}, inf_le_left := _, inf_le_right := _, le_inf := _, top := Sup set.univ, le_top := _, bot := Sup ∅, bot_le := _, Sup := Sup H2, Inf := λ (s : set α), Sup (lower_bounds s), le_Sup := _, Sup_le := _, Inf_le := _, le_Inf := _}

source

@[class]

structure complete_linear_order (α : Type u_6) :

Type u_6

sup : α → α → α
le : α → α → Prop
lt : α → α → Prop
le_refl : ∀ (a : α), a ≤ a
le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
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_1 : α), a ≤ c_1 → b ≤ c_1 → a ⊔ 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 ≤ b → a ≤ c_1 → a ≤ b ⊓ c_1
top : α
le_top : ∀ (a : α), a ≤ ⊤
bot : α
bot_le : ∀ (a : α), ⊥ ≤ a
Sup : set α → α
Inf : set α → α
le_Sup : ∀ (s : set α) (a : α), a ∈ s → a ≤ complete_linear_order.Sup s
Sup_le : ∀ (s : set α) (a : α), (∀ (b : α), b ∈ s → b ≤ a) → complete_linear_order.Sup s ≤ a
Inf_le : ∀ (s : set α) (a : α), a ∈ s → complete_linear_order.Inf s ≤ a
le_Inf : ∀ (s : set α) (a : α), (∀ (b : α), b ∈ s → a ≤ b) → a ≤ complete_linear_order.Inf s
le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a
decidable_le : decidable_rel has_le.le
decidable_eq : decidable_eq α
decidable_lt : decidable_rel has_lt.lt

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

Instances

source

@[instance]

def complete_linear_order.to_decidable_linear_order (α : Type u_6) [s : complete_linear_order α] :

decidable_linear_order α

source

@[instance]

def complete_linear_order.to_complete_lattice (α : Type u_6) [s : complete_linear_order α] :

complete_lattice α

source

@[instance]

def order_dual.complete_lattice (α : Type u_1) [complete_lattice α] :

complete_lattice (order_dual α)

Equations

order_dual.complete_lattice α = {sup := bounded_lattice.sup (order_dual.bounded_lattice α), le := bounded_lattice.le (order_dual.bounded_lattice α), lt := bounded_lattice.lt (order_dual.bounded_lattice α), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := bounded_lattice.inf (order_dual.bounded_lattice α), inf_le_left := _, inf_le_right := _, le_inf := _, top := bounded_lattice.top (order_dual.bounded_lattice α), le_top := _, bot := bounded_lattice.bot (order_dual.bounded_lattice α), bot_le := _, Sup := Sup (order_dual.has_Sup α), Inf := Inf (order_dual.has_Inf α), le_Sup := _, Sup_le := _, Inf_le := _, le_Inf := _}

source

@[instance]

def order_dual.complete_linear_order (α : Type u_1) [complete_linear_order α] :

complete_linear_order (order_dual α)

Equations

order_dual.complete_linear_order α = {sup := complete_lattice.sup (order_dual.complete_lattice α), le := complete_lattice.le (order_dual.complete_lattice α), lt := complete_lattice.lt (order_dual.complete_lattice α), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := complete_lattice.inf (order_dual.complete_lattice α), inf_le_left := _, inf_le_right := _, le_inf := _, top := complete_lattice.top (order_dual.complete_lattice α), le_top := _, bot := complete_lattice.bot (order_dual.complete_lattice α), bot_le := _, Sup := complete_lattice.Sup (order_dual.complete_lattice α), Inf := complete_lattice.Inf (order_dual.complete_lattice α), le_Sup := _, Sup_le := _, Inf_le := _, le_Inf := _, le_total := _, decidable_le := decidable_linear_order.decidable_le (order_dual.decidable_linear_order α), decidable_eq := decidable_linear_order.decidable_eq (order_dual.decidable_linear_order α), decidable_lt := decidable_linear_order.decidable_lt (order_dual.decidable_linear_order α)}

source

theorem le_Sup {α : Type u_1} [complete_lattice α] {s : set α} {a : α} (a_1 : a ∈ s) :

a ≤ Sup s

source

theorem Sup_le {α : Type u_1} [complete_lattice α] {s : set α} {a : α} (a_1 : ∀ (b : α), b ∈ s → b ≤ a) :

Sup s ≤ a

source

theorem Inf_le {α : Type u_1} [complete_lattice α] {s : set α} {a : α} (a_1 : a ∈ s) :

Inf s ≤ a

source

theorem le_Inf {α : Type u_1} [complete_lattice α] {s : set α} {a : α} (a_1 : ∀ (b : α), b ∈ s → a ≤ b) :

a ≤ Inf s

source

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

is_lub s (Sup s)

source

theorem is_lub.Sup_eq {α : Type u_1} [complete_lattice α] {s : set α} {a : α} (h : is_lub s a) :

Sup s = a

source

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

is_glb s (Inf s)

source

theorem is_glb.Inf_eq {α : Type u_1} [complete_lattice α] {s : set α} {a : α} (h : is_glb s a) :

Inf s = a

source

theorem le_Sup_of_le {α : Type u_1} [complete_lattice α] {s : set α} {a b : α} (hb : b ∈ s) (h : a ≤ b) :

a ≤ Sup s

source

theorem Inf_le_of_le {α : Type u_1} [complete_lattice α] {s : set α} {a b : α} (hb : b ∈ s) (h : b ≤ a) :

Inf s ≤ a

source

theorem Sup_le_Sup {α : Type u_1} [complete_lattice α] {s t : set α} (h : s ⊆ t) :

Sup s ≤ Sup t

source

theorem Inf_le_Inf {α : Type u_1} [complete_lattice α] {s t : set α} (h : s ⊆ t) :

Inf t ≤ Inf s

source

@[simp]

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

Sup s ≤ a ↔ ∀ (b : α), b ∈ s → b ≤ a

source

@[simp]

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

a ≤ Inf s ↔ ∀ (b : α), b ∈ s → a ≤ b

source

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

Sup s ≤ Sup t

source

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

Inf t ≤ Inf s

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_instert_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_singleton {α : Type u_1} [complete_lattice α] {a : α} :

Sup {a} = a

source

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

Inf {a} = a

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

@[simp]

theorem Sup_eq_bot {α : Type u_1} [complete_lattice α] {s : set α} :

Sup s = ⊥ ↔ ∀ (a : α), a ∈ s → a = ⊥

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 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

@[simp]

theorem supr_le_iff {α : Type u_1} {ι : Sort u_4} [complete_lattice α] {s : ι → α} {a : α} :

supr s ≤ a ↔ ∀ (i : ι), s i ≤ a

source

theorem Sup_eq_supr {α : Type u_1} [complete_lattice α] {s : set α} :

Sup s = ⨆ (a : α) (H : a ∈ s), a

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 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 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 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 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 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_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 supr_sup_eq {α : Type u_1} {β : Type u_2} [complete_lattice α] {f g : β → α} :

(⨆ (x : β), f x ⊔ g x) = (⨆ (x : β), f x) ⊔ ⨆ (x : β), g x

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

@[simp]

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

infi s = s trivial

source

@[simp]

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 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_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 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 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)

source

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

infi s = ⊤

source

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

supr s = ⊥

source

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

infi s = ⊤

source

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

supr s = ⊥

source

@[simp]

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

infi s = ⊤

source

@[simp]

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

supr s = ⊥

source

@[simp]

theorem infi_unit {α : Type u_1} [complete_lattice α] {f : unit → α} :

(⨅ (x : unit), f x) = f ()

source

@[simp]

theorem supr_unit {α : Type u_1} [complete_lattice α] {f : unit → α} :

(⨆ (x : unit), f x) = 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 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 Sup_eq_supr' {α : Type u_1} [complete_lattice α] {s : set α} :

Sup s = ⨆ (x : ↥s), ↑x

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_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 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)

source

@[instance]

def complete_lattice_Prop :

complete_lattice Prop

Equations

complete_lattice_Prop = {sup := bounded_distrib_lattice.sup bounded_distrib_lattice_Prop, le := bounded_distrib_lattice.le bounded_distrib_lattice_Prop, lt := bounded_distrib_lattice.lt bounded_distrib_lattice_Prop, le_refl := complete_lattice_Prop._proof_1, le_trans := complete_lattice_Prop._proof_2, lt_iff_le_not_le := complete_lattice_Prop._proof_3, le_antisymm := complete_lattice_Prop._proof_4, le_sup_left := complete_lattice_Prop._proof_5, le_sup_right := complete_lattice_Prop._proof_6, sup_le := complete_lattice_Prop._proof_7, inf := bounded_distrib_lattice.inf bounded_distrib_lattice_Prop, inf_le_left := complete_lattice_Prop._proof_8, inf_le_right := complete_lattice_Prop._proof_9, le_inf := complete_lattice_Prop._proof_10, top := bounded_distrib_lattice.top bounded_distrib_lattice_Prop, le_top := complete_lattice_Prop._proof_11, bot := bounded_distrib_lattice.bot bounded_distrib_lattice_Prop, bot_le := complete_lattice_Prop._proof_12, Sup := λ (s : set Prop), ∃ (a : Prop) (H : a ∈ s), a, Inf := λ (s : set Prop), ∀ (a : Prop), a ∈ s → a, le_Sup := complete_lattice_Prop._proof_13, Sup_le := complete_lattice_Prop._proof_14, Inf_le := complete_lattice_Prop._proof_15, le_Inf := complete_lattice_Prop._proof_16}

source

theorem Inf_Prop_eq {s : set Prop} :

Inf s = ∀ (p : Prop), p ∈ s → p

source

theorem Sup_Prop_eq {s : set Prop} :

Sup s = ∃ (p : Prop) (H : p ∈ s), p

source

theorem infi_Prop_eq {ι : Sort u_1} {p : ι → Prop} :

(⨅ (i : ι), p i) = ∀ (i : ι), p i

source

theorem supr_Prop_eq {ι : Sort u_1} {p : ι → Prop} :

(⨆ (i : ι), p i) = ∃ (i : ι), p i

source

@[instance]

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

has_Sup (Π (i : α), β i)

Equations

pi.has_Sup = {Sup := λ (s : set (Π (i : α), β i)) (i : α), ⨆ (f : ↥s), ↑f i}

source

@[instance]

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

has_Inf (Π (i : α), β i)

Equations

pi.has_Inf = {Inf := λ (s : set (Π (i : α), β i)) (i : α), ⨅ (f : ↥s), ↑f i}

source

@[instance]

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

complete_lattice (Π (i : α), β i)

Equations

pi.complete_lattice = {sup := bounded_lattice.sup pi.bounded_lattice, le := bounded_lattice.le pi.bounded_lattice, lt := bounded_lattice.lt pi.bounded_lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := bounded_lattice.inf pi.bounded_lattice, inf_le_left := _, inf_le_right := _, le_inf := _, top := bounded_lattice.top pi.bounded_lattice, le_top := _, bot := bounded_lattice.bot pi.bounded_lattice, bot_le := _, Sup := Sup pi.has_Sup, Inf := Inf pi.has_Inf, le_Sup := _, Sup_le := _, Inf_le := _, le_Inf := _}

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

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 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

@[instance]