Theory of complete lattices #
This file contains basic results on complete lattices.
Naming conventions #
In lemma names,
sSupis calledsSupsInfis calledsInf⨆ i, s iis callediSup⨅ i, s iis callediInf⨆ i j, s i jis callediSup₂. This is aniSupinside aniSup.⨅ i j, s i jis callediInf₂. This is aniInfinside aniInf.⨆ i ∈ s, t iis calledbiSupfor "boundediSup". This is the special case ofiSup₂wherej : i ∈ s.⨅ i ∈ s, t iis calledbiInffor "boundediInf". This is the special case ofiInf₂wherej : i ∈ s.
Notation #
theorem
sSup_le_sSup_of_isCofinalFor
{α : Type u_1}
[CompleteSemilatticeSup α]
{s t : Set α}
(h : IsCofinalFor s t)
:
theorem
sInf_le_sInf_of_isCoinitialFor
{α : Type u_1}
[CompleteSemilatticeInf α]
{s t : Set α}
(h : IsCoinitialFor s t)
:
@[simp]
@[simp]
theorem
sInf_le_sSup_of_nonempty_inter
{α : Type u_1}
[CompleteLattice α]
{s t : Set α}
(h : (s ∩ t).Nonempty)
:
@[simp]
@[simp]
theorem
sSup_le_sSup_of_subset_insert_bot
{α : Type u_1}
[CompleteLattice α]
{s t : Set α}
(h : s ⊆ insert ⊥ t)
:
theorem
sInf_le_sInf_of_subset_insert_top
{α : Type u_1}
[CompleteLattice α]
{s t : Set α}
(h : s ⊆ insert ⊤ t)
:
@[deprecated sSup_sdiff_singleton_bot (since := "2026-06-03")]
Alias of sSup_sdiff_singleton_bot.
theorem
sSup_eq_of_forall_le_of_forall_lt_exists_gt
{α : Type u_1}
[CompleteLattice α]
{s : Set α}
{b : α}
(h₁ : ∀ a ∈ s, a ≤ b)
(h₂ : ∀ w < b, ∃ a ∈ s, w < a)
:
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 csSup_eq_of_forall_le_of_forall_lt_exists_gt for a version in conditionally complete
lattices.
theorem
sInf_eq_of_forall_ge_of_forall_gt_exists_lt
{α : Type u_1}
[CompleteLattice α]
{s : Set α}
{b : α}
(h₁ : ∀ a ∈ s, b ≤ a)
(h₂ : ∀ (w : α), b < w → ∃ a ∈ s, a < w)
:
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 csInf_eq_of_forall_ge_of_forall_gt_exists_lt for a version in conditionally complete
lattices.
theorem
Function.Surjective.iSup_comp
{α : Type u_1}
{ι : Sort u_4}
{ι' : Sort u_5}
[SupSet α]
{f : ι → ι'}
(hf : Surjective f)
(g : ι' → α)
:
theorem
Function.Surjective.iInf_comp
{α : Type u_1}
{ι : Sort u_4}
{ι' : Sort u_5}
[InfSet α]
{f : ι → ι'}
(hf : Surjective f)
(g : ι' → α)
:
theorem
Function.Surjective.iSup_congr
{α : Type u_1}
{ι : Sort u_4}
{ι' : Sort u_5}
[SupSet α]
{f : ι → α}
{g : ι' → α}
(h : ι → ι')
(h1 : Surjective h)
(h2 : ∀ (x : ι), g (h x) = f x)
:
theorem
Function.Surjective.iInf_congr
{α : Type u_1}
{ι : Sort u_4}
{ι' : Sort u_5}
[InfSet α]
{f : ι → α}
{g : ι' → α}
(h : ι → ι')
(h1 : Surjective h)
(h2 : ∀ (x : ι), g (h x) = f x)
:
theorem
IsLUB.iSup_eq
{α : Type u_1}
{ι : Sort u_4}
[CompleteLattice α]
{f : ι → α}
{a : α}
(h : IsLUB (Set.range f) a)
:
theorem
IsGLB.iInf_eq
{α : Type u_1}
{ι : Sort u_4}
[CompleteLattice α]
{f : ι → α}
{a : α}
(h : IsGLB (Set.range f) a)
:
theorem
le_iSup_of_le
{α : Type u_1}
{ι : Sort u_4}
[CompleteLattice α]
{f : ι → α}
{a : α}
(i : ι)
(h : a ≤ f i)
:
theorem
iInf_le_of_le
{α : Type u_1}
{ι : Sort u_4}
[CompleteLattice α]
{f : ι → α}
{a : α}
(i : ι)
(h : f i ≤ a)
:
theorem
le_iSup₂_of_le
{α : Type u_1}
{ι : Sort u_4}
{κ : ι → Sort u_6}
[CompleteLattice α]
{a : α}
{f : (i : ι) → κ i → α}
(i : ι)
(j : κ i)
(h : a ≤ f i j)
:
theorem
iInf₂_le_of_le
{α : Type u_1}
{ι : Sort u_4}
{κ : ι → Sort u_6}
[CompleteLattice α]
{a : α}
{f : (i : ι) → κ i → α}
(i : ι)
(j : κ i)
(h : f i j ≤ a)
:
theorem
iSup₂_le_iSup
{α : Type u_1}
{ι : Sort u_4}
[CompleteLattice α]
(κ : ι → Sort u_8)
(f : ι → α)
:
theorem
iInf_le_iInf₂
{α : Type u_1}
{ι : Sort u_4}
[CompleteLattice α]
(κ : ι → Sort u_8)
(f : ι → α)
:
theorem
iSup₂_mono
{α : Type u_1}
{ι : Sort u_4}
{κ : ι → Sort u_6}
[CompleteLattice α]
{f g : (i : ι) → κ i → α}
(h : ∀ (i : ι) (j : κ i), f i j ≤ g i j)
:
theorem
iInf₂_mono
{α : Type u_1}
{ι : Sort u_4}
{κ : ι → Sort u_6}
[CompleteLattice α]
{f g : (i : ι) → κ i → α}
(h : ∀ (i : ι) (j : κ i), g i j ≤ f i j)
:
theorem
iSup_mono'
{α : Type u_1}
{ι : Sort u_4}
{ι' : Sort u_5}
[CompleteLattice α]
{f : ι → α}
{g : ι' → α}
(h : ∀ (i : ι), ∃ (i' : ι'), f i ≤ g i')
:
theorem
iInf_mono'
{α : Type u_1}
{ι : Sort u_4}
{ι' : Sort u_5}
[CompleteLattice α]
{f : ι → α}
{g : ι' → α}
(h : ∀ (i : ι), ∃ (i' : ι'), g i' ≤ f i)
:
theorem
iSup₂_mono'
{α : Type u_1}
{ι : Sort u_4}
{ι' : Sort u_5}
{κ : ι → Sort u_6}
{κ' : ι' → Sort u_7}
[CompleteLattice α]
{f : (i : ι) → κ i → α}
{g : (i' : ι') → κ' i' → α}
(h : ∀ (i : ι) (j : κ i), ∃ (i' : ι') (j' : κ' i'), f i j ≤ g i' j')
:
theorem
iInf₂_mono'
{α : Type u_1}
{ι : Sort u_4}
{ι' : Sort u_5}
{κ : ι → Sort u_6}
{κ' : ι' → Sort u_7}
[CompleteLattice α]
{f : (i : ι) → κ i → α}
{g : (i' : ι') → κ' i' → α}
(h : ∀ (i : ι) (j : κ i), ∃ (i' : ι') (j' : κ' i'), g i' j' ≤ f i j)
:
theorem
iSup_const_mono
{α : Type u_1}
{ι : Sort u_4}
{ι' : Sort u_5}
[CompleteLattice α]
{a : α}
(h : ι → ι')
:
theorem
iInf_const_mono
{α : Type u_1}
{ι : Sort u_4}
{ι' : Sort u_5}
[CompleteLattice α]
{a : α}
(h : ι → ι')
:
theorem
iSup_iInf_le_iInf_iSup
{α : Type u_1}
{ι : Sort u_4}
{ι' : Sort u_5}
[CompleteLattice α]
(f : ι → ι' → α)
:
theorem
biSup_mono
{α : Type u_1}
{ι : Sort u_4}
[CompleteLattice α]
{f : ι → α}
{p q : ι → Prop}
(hpq : ∀ (i : ι), p i → q i)
:
theorem
biInf_mono
{α : Type u_1}
{ι : Sort u_4}
[CompleteLattice α]
{f : ι → α}
{p q : ι → Prop}
(hpq : ∀ (i : ι), p i → q i)
:
@[simp]
@[simp]
theorem
iSup₂_le_iff
{α : Type u_1}
{ι : Sort u_4}
{κ : ι → Sort u_6}
[CompleteLattice α]
{a : α}
{f : (i : ι) → κ i → α}
:
theorem
le_iInf₂_iff
{α : Type u_1}
{ι : Sort u_4}
{κ : ι → Sort u_6}
[CompleteLattice α]
{a : α}
{f : (i : ι) → κ i → α}
:
@[deprecated sInf_upperBounds_eq_sSup (since := "2026-02-01")]
Alias of sInf_upperBounds_eq_sSup.
theorem
Monotone.le_map_iSup
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
[CompleteLattice α]
{s : ι → α}
[CompleteLattice β]
{f : α → β}
(hf : Monotone f)
:
theorem
Monotone.map_iInf_le
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
[CompleteLattice α]
{s : ι → α}
[CompleteLattice β]
{f : α → β}
(hf : Monotone f)
:
theorem
Antitone.le_map_iInf
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
[CompleteLattice α]
{s : ι → α}
[CompleteLattice β]
{f : α → β}
(hf : Antitone f)
:
theorem
Antitone.map_iSup_le
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
[CompleteLattice α]
{s : ι → α}
[CompleteLattice β]
{f : α → β}
(hf : Antitone f)
:
theorem
Monotone.le_map_iSup₂
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
{κ : ι → Sort u_6}
[CompleteLattice α]
[CompleteLattice β]
{f : α → β}
(hf : Monotone f)
(s : (i : ι) → κ i → α)
:
theorem
Monotone.map_iInf₂_le
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
{κ : ι → Sort u_6}
[CompleteLattice α]
[CompleteLattice β]
{f : α → β}
(hf : Monotone f)
(s : (i : ι) → κ i → α)
:
theorem
Antitone.le_map_iInf₂
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
{κ : ι → Sort u_6}
[CompleteLattice α]
[CompleteLattice β]
{f : α → β}
(hf : Antitone f)
(s : (i : ι) → κ i → α)
:
theorem
Antitone.map_iSup₂_le
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
{κ : ι → Sort u_6}
[CompleteLattice α]
[CompleteLattice β]
{f : α → β}
(hf : Antitone f)
(s : (i : ι) → κ i → α)
:
theorem
Monotone.le_map_sSup
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
[CompleteLattice β]
{s : Set α}
{f : α → β}
(hf : Monotone f)
:
theorem
Monotone.map_sInf_le
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
[CompleteLattice β]
{s : Set α}
{f : α → β}
(hf : Monotone f)
:
theorem
Antitone.le_map_sInf
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
[CompleteLattice β]
{s : Set α}
{f : α → β}
(hf : Antitone f)
:
theorem
Antitone.map_sSup_le
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
[CompleteLattice β]
{s : Set α}
{f : α → β}
(hf : Antitone f)
:
theorem
OrderIso.map_iSup
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
[CompleteLattice α]
[CompleteLattice β]
(f : α ≃o β)
(x : ι → α)
:
theorem
OrderIso.map_iInf
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
[CompleteLattice α]
[CompleteLattice β]
(f : α ≃o β)
(x : ι → α)
:
theorem
OrderIso.map_iSup₂
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
{κ : ι → Sort u_6}
[CompleteLattice α]
[CompleteLattice β]
(f : α ≃o β)
(x : (i : ι) → κ i → α)
:
theorem
OrderIso.map_iInf₂
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
{κ : ι → Sort u_6}
[CompleteLattice α]
[CompleteLattice β]
(f : α ≃o β)
(x : (i : ι) → κ i → α)
:
theorem
OrderIso.map_sSup
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
[CompleteLattice β]
(f : α ≃o β)
(s : Set α)
:
theorem
OrderIso.map_sInf
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
[CompleteLattice β]
(f : α ≃o β)
(s : Set α)
:
theorem
iSup_comp_le
{α : Type u_1}
{ι : Sort u_4}
[CompleteLattice α]
{ι' : Sort u_8}
(f : ι' → α)
(g : ι → ι')
:
theorem
le_iInf_comp
{α : Type u_1}
{ι : Sort u_4}
[CompleteLattice α]
{ι' : Sort u_8}
(f : ι' → α)
(g : ι → ι')
:
theorem
Monotone.iSup_comp_eq
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
[CompleteLattice α]
[Preorder β]
{f : β → α}
(hf : Monotone f)
{s : ι → β}
(hs : ∀ (x : β), ∃ (i : ι), x ≤ s i)
:
theorem
Monotone.iInf_comp_eq
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
[CompleteLattice α]
[Preorder β]
{f : β → α}
(hf : Monotone f)
{s : ι → β}
(hs : ∀ (x : β), ∃ (i : ι), s i ≤ x)
:
@[simp]
@[simp]
theorem
iSup_eq_of_forall_le_of_forall_lt_exists_gt
{α : Type u_1}
{ι : Sort u_4}
[CompleteLattice α]
{b : α}
{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 ciSup_eq_of_forall_le_of_forall_lt_exists_gt for a version in conditionally complete
lattices.
theorem
iInf_eq_of_forall_ge_of_forall_gt_exists_lt
{α : Type u_1}
{ι : Sort u_4}
[CompleteLattice α]
{b : α}
{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 ciInf_eq_of_forall_ge_of_forall_gt_exists_lt for a version in conditionally complete
lattices.
theorem
iSup₂_comm
{α : Type u_1}
[CompleteLattice α]
{ι₁ : Sort u_8}
{ι₂ : Sort u_9}
{κ₁ : ι₁ → Sort u_10}
{κ₂ : ι₂ → Sort u_11}
(f : (i₁ : ι₁) → κ₁ i₁ → (i₂ : ι₂) → κ₂ i₂ → α)
:
⨆ (i₁ : ι₁), ⨆ (j₁ : κ₁ i₁), ⨆ (i₂ : ι₂), ⨆ (j₂ : κ₂ i₂), f i₁ j₁ i₂ j₂ = ⨆ (i₂ : ι₂), ⨆ (j₂ : κ₂ i₂), ⨆ (i₁ : ι₁), ⨆ (j₁ : κ₁ i₁), f i₁ j₁ i₂ j₂
theorem
iInf₂_comm
{α : Type u_1}
[CompleteLattice α]
{ι₁ : Sort u_8}
{ι₂ : Sort u_9}
{κ₁ : ι₁ → Sort u_10}
{κ₂ : ι₂ → Sort u_11}
(f : (i₁ : ι₁) → κ₁ i₁ → (i₂ : ι₂) → κ₂ i₂ → α)
:
⨅ (i₁ : ι₁), ⨅ (j₁ : κ₁ i₁), ⨅ (i₂ : ι₂), ⨅ (j₂ : κ₂ i₂), f i₁ j₁ i₂ j₂ = ⨅ (i₂ : ι₂), ⨅ (j₂ : κ₂ i₂), ⨅ (i₁ : ι₁), ⨅ (j₁ : κ₁ i₁), f i₁ j₁ i₂ j₂
@[simp]
theorem
iSup_iSup_eq_left
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
{b : β}
{f : (x : β) → x = b → α}
:
@[simp]
theorem
iInf_iInf_eq_left
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
{b : β}
{f : (x : β) → x = b → α}
:
@[simp]
theorem
iSup_iSup_eq_right
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
{b : β}
{f : (x : β) → b = x → α}
:
@[simp]
theorem
iInf_iInf_eq_right
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
{b : β}
{f : (x : β) → b = x → α}
:
theorem
iSup_subtype'
{α : Type u_1}
{ι : Sort u_4}
[CompleteLattice α]
{p : ι → Prop}
{f : (i : ι) → p i → α}
:
theorem
iInf_subtype'
{α : Type u_1}
{ι : Sort u_4}
[CompleteLattice α]
{p : ι → Prop}
{f : (i : ι) → p i → α}
:
theorem
biSup_const
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
{a : α}
{s : Set β}
(hs : s.Nonempty)
:
theorem
biInf_const
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
{a : α}
{s : Set β}
(hs : s.Nonempty)
:
theorem
biInf_le_biSup
{α : Type u_1}
[CompleteLattice α]
{ι : Type u_8}
{s : Set ι}
(hs : s.Nonempty)
{f : ι → α}
:
theorem
biSup_lt_eq_iSup
{α : Type u_1}
[CompleteLattice α]
{ι : Type u_8}
[LT ι]
[NoMaxOrder ι]
{f : ι → α}
:
theorem
biInf_lt_eq_iInf
{α : Type u_1}
[CompleteLattice α]
{ι : Type u_8}
[LT ι]
[NoMaxOrder ι]
{f : ι → α}
:
theorem
biSup_le_eq_iSup
{α : Type u_1}
[CompleteLattice α]
{ι : Type u_8}
[Preorder ι]
{f : ι → α}
:
theorem
biInf_le_eq_iInf
{α : Type u_1}
[CompleteLattice α]
{ι : Type u_8}
[Preorder ι]
{f : ι → α}
:
theorem
biSup_gt_eq_iSup
{α : Type u_1}
[CompleteLattice α]
{ι : Type u_8}
[LT ι]
[NoMinOrder ι]
{f : ι → α}
:
theorem
biInf_gt_eq_iInf
{α : Type u_1}
[CompleteLattice α]
{ι : Type u_8}
[LT ι]
[NoMinOrder ι]
{f : ι → α}
:
theorem
biSup_ge_eq_iSup
{α : Type u_1}
[CompleteLattice α]
{ι : Type u_8}
[Preorder ι]
{f : ι → α}
:
theorem
biInf_ge_eq_iInf
{α : Type u_1}
[CompleteLattice α]
{ι : Type u_8}
[Preorder ι]
{f : ι → α}
:
theorem
biSup_le_eq_of_monotone
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
[Preorder β]
{f : β → α}
(hf : Monotone f)
(b : β)
:
theorem
biInf_ge_eq_of_monotone
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
[Preorder β]
{f : β → α}
(hf : Monotone f)
(b : β)
:
theorem
biInf_le_eq_of_antitone
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
[Preorder β]
{f : β → α}
(hf : Antitone f)
(b : β)
:
theorem
biSup_ge_eq_of_antitone
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
[Preorder β]
{f : β → α}
(hf : Antitone f)
(b : β)
:
@[simp]
theorem
iSup_exists
{α : Type u_1}
{ι : Sort u_4}
[CompleteLattice α]
{p : ι → Prop}
{f : Exists p → α}
:
@[simp]
theorem
iInf_exists
{α : Type u_1}
{ι : Sort u_4}
[CompleteLattice α]
{p : ι → Prop}
{f : Exists p → α}
:
theorem
iSup_dite
{α : Type u_1}
{ι : Sort u_4}
[CompleteLattice α]
(p : ι → Prop)
[DecidablePred p]
(f : (i : ι) → p i → α)
(g : (i : ι) → ¬p i → α)
:
theorem
iInf_dite
{α : Type u_1}
{ι : Sort u_4}
[CompleteLattice α]
(p : ι → Prop)
[DecidablePred p]
(f : (i : ι) → p i → α)
(g : (i : ι) → ¬p i → α)
:
theorem
iSup_range
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
[CompleteLattice α]
{g : β → α}
{f : ι → β}
:
theorem
iInf_range
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
[CompleteLattice α]
{g : β → α}
{f : ι → β}
:
theorem
OrderIso.map_sSup_eq_sSup_symm_preimage
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
[CompleteLattice β]
(f : α ≃o β)
(s : Set α)
:
theorem
OrderIso.map_sInf_eq_sInf_symm_preimage
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
[CompleteLattice β]
(f : α ≃o β)
(s : Set α)
:
theorem
iSup_le_iSup_of_subset
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
{f : β → α}
{s t : Set β}
:
s ⊆ t → ⨆ x ∈ s, f x ≤ ⨆ x ∈ t, f x
theorem
iInf_le_iInf_of_subset
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
{f : β → α}
{s t : Set β}
:
s ⊆ t → ⨅ x ∈ t, f x ≤ ⨅ x ∈ s, f x
theorem
iSup_insert
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
{f : β → α}
{s : Set β}
{b : β}
:
theorem
iInf_insert
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
{f : β → α}
{s : Set β}
{b : β}
:
theorem
iSup_image
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
{γ : Type u_8}
{f : β → γ}
{g : γ → α}
{t : Set β}
:
theorem
iInf_image
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
{γ : Type u_8}
{f : β → γ}
{g : γ → α}
{t : Set β}
:
theorem
iSup_extend_bot
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
[CompleteLattice α]
{e : ι → β}
(he : Function.Injective e)
(f : ι → α)
:
theorem
iInf_extend_top
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
[CompleteLattice α]
{e : ι → β}
(he : Function.Injective e)
(f : ι → α)
:
theorem
Set.BijOn.iSup_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[CompleteLattice α]
{s : Set β}
{t : Set γ}
{f : β → γ}
(g : γ → α)
(hf : BijOn f s t)
:
theorem
Set.BijOn.iInf_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[CompleteLattice α]
{s : Set β}
{t : Set γ}
{f : β → γ}
(g : γ → α)
(hf : BijOn f s t)
:
theorem
biSup_le_eq_sup
{α : Type u_1}
[CompleteLattice α]
{ι : Type u_8}
[PartialOrder ι]
(f : ι → α)
(i : ι)
:
theorem
biInf_le_eq_inf
{α : Type u_1}
[CompleteLattice α]
{ι : Type u_8}
[PartialOrder ι]
(f : ι → α)
(i : ι)
:
theorem
biSup_ge_eq_sup
{α : Type u_1}
[CompleteLattice α]
{ι : Type u_8}
[PartialOrder ι]
(f : ι → α)
(i : ι)
:
theorem
biInf_ge_eq_inf
{α : Type u_1}
[CompleteLattice α]
{ι : Type u_8}
[PartialOrder ι]
(f : ι → α)
(i : ι)
:
theorem
iSup_sigma'
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
{κ : β → Type u_8}
(f : (i : β) → κ i → α)
:
theorem
iInf_sigma'
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
{κ : β → Type u_8}
(f : (i : β) → κ i → α)
:
theorem
iSup_psigma
{α : Type u_1}
[CompleteLattice α]
{ι : Sort u_8}
{κ : ι → Sort u_9}
(f : (i : ι) ×' κ i → α)
:
theorem
iInf_psigma
{α : Type u_1}
[CompleteLattice α]
{ι : Sort u_8}
{κ : ι → Sort u_9}
(f : (i : ι) ×' κ i → α)
:
theorem
iSup_psigma'
{α : Type u_1}
[CompleteLattice α]
{ι : Sort u_8}
{κ : ι → Sort u_9}
(f : (i : ι) → κ i → α)
:
theorem
iInf_psigma'
{α : Type u_1}
[CompleteLattice α]
{ι : Sort u_8}
{κ : ι → Sort u_9}
(f : (i : ι) → κ i → α)
:
theorem
iSup_prod'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[CompleteLattice α]
(f : β → γ → α)
:
theorem
iInf_prod'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[CompleteLattice α]
(f : β → γ → α)
:
theorem
biSup_prod'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[CompleteLattice α]
{f : β → γ → α}
{s : Set β}
{t : Set γ}
:
theorem
biInf_prod'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[CompleteLattice α]
{f : β → γ → α}
{s : Set β}
{t : Set γ}
:
theorem
iSup_image2
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
{γ : Type u_8}
{δ : Type u_9}
(f : β → γ → δ)
(s : Set β)
(t : Set γ)
(g : δ → α)
:
theorem
iInf_image2
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
{γ : Type u_8}
{δ : Type u_9}
(f : β → γ → δ)
(s : Set β)
(t : Set γ)
(g : δ → α)
:
A version of iSup_option useful for rewriting right-to-left.
A version of iInf_option useful for rewriting right-to-left.
theorem
sSup_image2
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[CompleteLattice α]
{f : β → γ → α}
{s : Set β}
{t : Set γ}
:
theorem
sInf_image2
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[CompleteLattice α]
{f : β → γ → α}
{s : Set β}
{t : Set γ}
:
Instances #
@[instance_reducible]
Equations
- One or more equations did not get rendered due to their size.
@[instance_reducible]
Equations
- One or more equations did not get rendered due to their size.
@[instance_reducible]
instance
Pi.instCompleteLattice
{α : Type u_8}
{β : α → Type u_9}
[(i : α) → CompleteLattice (β i)]
:
CompleteLattice ((i : α) → β i)
Equations
- Pi.instCompleteLattice = { toLattice := Pi.instLattice, toSupSet := Pi.supSet, isLUB_sSup := ⋯, toInfSet := Pi.infSet, isGLB_sInf := ⋯, toBoundedOrder := Pi.instBoundedOrder }
theorem
Monotone.sSup
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[CompleteLattice β]
{s : Set (α → β)}
(hs : ∀ f ∈ s, Monotone f)
:
theorem
Monotone.sInf
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[CompleteLattice β]
{s : Set (α → β)}
(hs : ∀ f ∈ s, Monotone f)
:
theorem
Antitone.sSup
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[CompleteLattice β]
{s : Set (α → β)}
(hs : ∀ f ∈ s, Antitone f)
:
theorem
Antitone.sInf
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[CompleteLattice β]
{s : Set (α → β)}
(hs : ∀ f ∈ s, Antitone f)
:
theorem
Monotone.iSup
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
[Preorder α]
[CompleteLattice β]
{f : ι → α → β}
(hf : ∀ (i : ι), Monotone (f i))
:
Monotone (⨆ (i : ι), f i)
theorem
Monotone.iInf
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
[Preorder α]
[CompleteLattice β]
{f : ι → α → β}
(hf : ∀ (i : ι), Monotone (f i))
:
Monotone (⨅ (i : ι), f i)
theorem
Antitone.iSup
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
[Preorder α]
[CompleteLattice β]
{f : ι → α → β}
(hf : ∀ (i : ι), Antitone (f i))
:
Antitone (⨆ (i : ι), f i)
theorem
Antitone.iInf
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_4}
[Preorder α]
[CompleteLattice β]
{f : ι → α → β}
(hf : ∀ (i : ι), Antitone (f i))
:
Antitone (⨅ (i : ι), f i)
@[instance_reducible]
instance
Prod.instCompleteLattice
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
[CompleteLattice β]
:
CompleteLattice (α × β)
Equations
- One or more equations did not get rendered due to their size.
@[reducible, inline]
abbrev
Function.Injective.completeLattice
{α : Type u_1}
{β : Type u_2}
[Max α]
[Min α]
[LE α]
[LT α]
[SupSet α]
[InfSet α]
[Top α]
[Bot α]
[CompleteLattice β]
(f : α → β)
(hf : Injective f)
(le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y)
(lt : ∀ {x y : α}, f x < f y ↔ x < y)
(map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b)
(map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b)
(map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a)
(map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a)
(map_top : f ⊤ = ⊤)
(map_bot : f ⊥ = ⊥)
:
Pullback a CompleteLattice along an injection.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
Transfer CompleteLattice across an Equiv.
Equations
- e.completeLattice = Function.Injective.completeLattice ⇑e ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯