Indexed sup / inf in conditionally complete lattices #
This file proves lemmas about iSup and iInf for functions valued in a conditionally complete
partial order, as opposed to a conditionally complete lattice.
TODO #
- Use
@[to_dual]in theGaloisConnectionandOrderIsosections.
theorem
DirectedOn.isLUB_ciSup_set
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompletePartialOrderSup α]
{f : β → α}
{s : Set β}
(hd : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) (f '' s))
(H : BddAbove (f '' s))
(Hne : s.Nonempty)
:
theorem
DirectedOn.isGLB_ciInf_set
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompletePartialOrderInf α]
{f : β → α}
{s : Set β}
(hd : DirectedOn (fun (x1 x2 : α) => x2 ≤ x1) (f '' s))
(H : BddBelow (f '' s))
(Hne : s.Nonempty)
:
theorem
DirectedOn.ciSup_set_le_iff
{α : Type u_1}
[ConditionallyCompletePartialOrderSup α]
{ι : Type u_5}
{s : Set ι}
{f : ι → α}
{a : α}
(hs : s.Nonempty)
(hd : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) (f '' s))
(hf : BddAbove (f '' s))
:
theorem
DirectedOn.le_ciInf_set_iff
{α : Type u_1}
[ConditionallyCompletePartialOrderInf α]
{ι : Type u_5}
{s : Set ι}
{f : ι → α}
{a : α}
(hs : s.Nonempty)
(hd : DirectedOn (fun (x1 x2 : α) => x2 ≤ x1) (f '' s))
(hf : BddBelow (f '' s))
:
theorem
Directed.ciSup_mono
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompletePartialOrderSup α]
{f g : ι → α}
(hdf : Directed (fun (x1 x2 : α) => x1 ≤ x2) f)
(hdg : Directed (fun (x1 x2 : α) => x1 ≤ x2) g)
(B : BddAbove (Set.range g))
(H : ∀ (x : ι), f x ≤ g x)
:
The indexed suprema of two functions are comparable if the functions are pointwise comparable
theorem
Directed.ciInf_mono
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompletePartialOrderInf α]
{f g : ι → α}
(hdf : Directed (fun (x1 x2 : α) => x2 ≤ x1) f)
(hdg : Directed (fun (x1 x2 : α) => x2 ≤ x1) g)
(B : BddBelow (Set.range g))
(H : ∀ (x : ι), g x ≤ f x)
:
The indexed infimum of two functions are comparable if the functions are pointwise comparable
theorem
DirectedOn.le_ciSup_set
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompletePartialOrderSup α]
{f : β → α}
{s : Set β}
(hd : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) (f '' s))
(H : BddAbove (f '' s))
{c : β}
(hc : c ∈ s)
:
theorem
DirectedOn.ciInf_set_le
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompletePartialOrderInf α]
{f : β → α}
{s : Set β}
(hd : DirectedOn (fun (x1 x2 : α) => x2 ≤ x1) (f '' s))
(H : BddBelow (f '' s))
{c : β}
(hc : c ∈ s)
:
@[simp]
theorem
ciSup_const
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompletePartialOrderSup α]
[hι : Nonempty ι]
{a : α}
:
@[simp]
theorem
ciInf_const
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompletePartialOrderInf α]
[hι : Nonempty ι]
{a : α}
:
@[simp]
theorem
ciSup_unique
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompletePartialOrderSup α]
[Unique ι]
{s : ι → α}
:
@[simp]
theorem
ciInf_unique
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompletePartialOrderInf α]
[Unique ι]
{s : ι → α}
:
theorem
ciSup_subsingleton
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompletePartialOrderSup α]
[Subsingleton ι]
(i : ι)
(s : ι → α)
:
theorem
ciInf_subsingleton
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompletePartialOrderInf α]
[Subsingleton ι]
(i : ι)
(s : ι → α)
:
theorem
ciSup_eq_ite
{α : Type u_1}
[ConditionallyCompletePartialOrderSup α]
{p : Prop}
[Decidable p]
{f : p → α}
:
theorem
ciInf_eq_ite
{α : Type u_1}
[ConditionallyCompletePartialOrderInf α]
{p : Prop}
[Decidable p]
{f : p → α}
:
theorem
Directed.ciSup_eq_of_forall_le_of_forall_lt_exists_gt
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompletePartialOrderSup α]
{b : α}
[Nonempty ι]
{f : ι → α}
(hd : Directed (fun (x1 x2 : α) => x1 ≤ x2) f)
(h₁ : ∀ (i : ι), f i ≤ b)
(h₂ : ∀ w < b, ∃ (i : ι), w < f i)
:
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 iSup_eq_of_forall_le_of_forall_lt_exists_gt for a version in complete lattices.
theorem
Directed.ciInf_eq_of_forall_ge_of_forall_gt_exists_lt
{α : Type u_1}
{ι : Sort u_4}
[ConditionallyCompletePartialOrderInf α]
{b : α}
[Nonempty ι]
{f : ι → α}
(hd : Directed (fun (x1 x2 : α) => x2 ≤ x1) f)
(h₁ : ∀ (i : ι), b ≤ f i)
(h₂ : ∀ (w : α), b < w → ∃ (i : ι), f i < w)
:
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 iInf_eq_of_forall_ge_of_forall_gt_exists_lt for a version in complete lattices.
theorem
Monotone.ciSup_mem_iInter_Icc_of_antitone
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompletePartialOrderSup α]
[Preorder β]
[IsDirectedOrder β]
{f g : β → α}
(hf : Monotone f)
(hg : Antitone g)
(h : f ≤ g)
:
Nested intervals lemma: if f is a monotone sequence, g is an antitone sequence, and
f n ≤ g n for all n, then ⨆ n, f n belongs to all the intervals [f n, g n].
theorem
ciSup_mem_iInter_Icc_of_antitone_Icc
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompletePartialOrderSup α]
[Preorder β]
[IsDirectedOrder β]
{f g : β → α}
(h : Antitone fun (n : β) => Set.Icc (f n) (g n))
(h' : ∀ (n : β), f n ≤ g n)
:
Nested intervals lemma: if [f n, g n] is an antitone sequence of nonempty
closed intervals, then ⨆ n, f n belongs to all the intervals [f n, g n].
theorem
GaloisConnection.l_csSup_of_directedOn'
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompletePartialOrderSup α]
[ConditionallyCompletePartialOrderSup β]
{l : α → β}
{u : β → α}
(gc : GaloisConnection l u)
{s : Set α}
(hd : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) s)
(hne : s.Nonempty)
(hbdd : BddAbove s)
:
theorem
GaloisConnection.l_csSup_of_directedOn
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompletePartialOrderSup α]
[ConditionallyCompletePartialOrderSup β]
{l : α → β}
{u : β → α}
(gc : GaloisConnection l u)
{s : Set α}
(hd : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) s)
(hne : s.Nonempty)
(hbdd : BddAbove s)
:
theorem
GaloisConnection.l_ciSup_of_directed
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
[ConditionallyCompletePartialOrderSup α]
[ConditionallyCompletePartialOrderSup β]
[Nonempty ι]
{l : α → β}
{u : β → α}
(gc : GaloisConnection l u)
{f : ι → α}
(hd : Directed (fun (x1 x2 : α) => x1 ≤ x2) f)
(hf : BddAbove (Set.range f))
:
theorem
GaloisConnection.l_ciSup_set_of_directedOn
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[ConditionallyCompletePartialOrderSup α]
[ConditionallyCompletePartialOrderSup β]
{l : α → β}
{u : β → α}
(gc : GaloisConnection l u)
{s : Set γ}
{f : γ → α}
(hd : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) (f '' s))
(hf : BddAbove (f '' s))
(hne : s.Nonempty)
:
theorem
GaloisConnection.u_csInf_of_directedOn
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompletePartialOrderInf α]
[ConditionallyCompletePartialOrderInf β]
{l : α → β}
{u : β → α}
(gc : GaloisConnection l u)
{s : Set β}
(hd : DirectedOn (fun (x1 x2 : β) => x1 ≥ x2) s)
(hne : s.Nonempty)
(hbdd : BddBelow s)
:
theorem
GaloisConnection.u_csInf_of_directedOn'
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompletePartialOrderInf α]
[ConditionallyCompletePartialOrderInf β]
{l : α → β}
{u : β → α}
(gc : GaloisConnection l u)
{s : Set β}
(hd : DirectedOn (fun (x1 x2 : β) => x1 ≥ x2) s)
(hne : s.Nonempty)
(hbdd : BddBelow s)
:
theorem
GaloisConnection.u_ciInf_of_directed
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
[ConditionallyCompletePartialOrderInf α]
[ConditionallyCompletePartialOrderInf β]
[Nonempty ι]
{l : α → β}
{u : β → α}
(gc : GaloisConnection l u)
{f : ι → β}
(hd : Directed (fun (x1 x2 : β) => x1 ≥ x2) f)
(hf : BddBelow (Set.range f))
:
theorem
GaloisConnection.u_ciInf_set_of_directedOn
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[ConditionallyCompletePartialOrderInf α]
[ConditionallyCompletePartialOrderInf β]
{l : α → β}
{u : β → α}
(gc : GaloisConnection l u)
{s : Set γ}
{f : γ → β}
(hd : DirectedOn (fun (x1 x2 : β) => x1 ≥ x2) (f '' s))
(hf : BddBelow (f '' s))
(hne : s.Nonempty)
:
theorem
OrderIso.map_csSup_of_directedOn
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompletePartialOrderSup α]
[ConditionallyCompletePartialOrderSup β]
(e : α ≃o β)
{s : Set α}
(hd : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) s)
(hne : s.Nonempty)
(hbdd : BddAbove s)
:
theorem
OrderIso.map_csSup_of_directedOn'
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompletePartialOrderSup α]
[ConditionallyCompletePartialOrderSup β]
(e : α ≃o β)
{s : Set α}
(hd : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) s)
(hne : s.Nonempty)
(hbdd : BddAbove s)
:
theorem
OrderIso.map_ciSup_of_directed
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
[ConditionallyCompletePartialOrderSup α]
[ConditionallyCompletePartialOrderSup β]
[Nonempty ι]
(e : α ≃o β)
{f : ι → α}
(hd : Directed (fun (x1 x2 : α) => x1 ≤ x2) f)
(hf : BddAbove (Set.range f))
:
theorem
OrderIso.map_ciSup_set_of_directedOn
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[ConditionallyCompletePartialOrderSup α]
[ConditionallyCompletePartialOrderSup β]
(e : α ≃o β)
{s : Set γ}
{f : γ → α}
(hd : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) (f '' s))
(hf : BddAbove (f '' s))
(hne : s.Nonempty)
:
theorem
OrderIso.map_csInf_of_directedOn
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompletePartialOrderInf α]
[ConditionallyCompletePartialOrderInf β]
(e : α ≃o β)
{s : Set α}
(hd : DirectedOn (fun (x1 x2 : α) => x1 ≥ x2) s)
(hne : s.Nonempty)
(hbdd : BddBelow s)
:
theorem
OrderIso.map_csInf_of_directedOn'
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompletePartialOrderInf α]
[ConditionallyCompletePartialOrderInf β]
(e : α ≃o β)
{s : Set α}
(hd : DirectedOn (fun (x1 x2 : α) => x1 ≥ x2) s)
(hne : s.Nonempty)
(hbdd : BddBelow s)
:
theorem
OrderIso.map_ciInf_of_directed
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
[ConditionallyCompletePartialOrderInf α]
[ConditionallyCompletePartialOrderInf β]
[Nonempty ι]
(e : α ≃o β)
{f : ι → α}
(hd : Directed (fun (x1 x2 : α) => x1 ≥ x2) f)
(hf : BddBelow (Set.range f))
:
theorem
OrderIso.map_ciInf_set_of_directedOn
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[ConditionallyCompletePartialOrderInf α]
[ConditionallyCompletePartialOrderInf β]
(e : α ≃o β)
{s : Set γ}
{f : γ → α}
(hd : DirectedOn (fun (x1 x2 : α) => x1 ≥ x2) (f '' s))
(hf : BddBelow (f '' s))
(hne : s.Nonempty)
: