# Lattice operations on finsets #

This file is concerned with folding binary lattice operations over finsets.

For the special case of maximum and minimum of a finset, see Max.lean.

See also `Mathlib/Order/CompleteLattice/Finset.lean`, which is instead concerned with how big lattice or set operations behave when indexed by a finset.

### sup #

source
def Finset.sup {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] (s : Finset β) (f : β → α) :
α

Supremum of a finite set: `sup {a, b, c} f = f a ⊔ f b ⊔ f c`

Equations

- s.sup f = Finset.fold (fun (x1 x2 : α) => x1 ⊔ x2) ⊥ f s

Instances For

source
theorem Finset.sup_def {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} {f : β → α} :
s.sup f = (Multiset.map f s.val).sup
source
@[simp]
theorem Finset.sup_empty {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {f : β → α} :
∅.sup f = ⊥
source
@[simp]
theorem Finset.sup_cons {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} {f : β → α} {b : β} (h : b ∉ s) :
(cons b s h).sup f = f b ⊔ s.sup f
source
@[simp]
theorem Finset.sup_insert {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} {f : β → α} [DecidableEq β] {b : β} :
(insert b s).sup f = f b ⊔ s.sup f
source
@[simp]
theorem Finset.sup_image {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeSup α] [OrderBot α] [DecidableEq β] (s : Finset γ) (f : γ → β) (g : β → α) :
(image f s).sup g = s.sup (g ∘ f)
source
@[simp]
theorem Finset.sup_map {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeSup α] [OrderBot α] (s : Finset γ) (f : γ ↪ β) (g : β → α) :
(map f s).sup g = s.sup (g ∘ ⇑f)
source
@[simp]
theorem Finset.sup_singleton {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {f : β → α} {b : β} :
{b}.sup f = f b
source
theorem Finset.sup_sup {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} {f g : β → α} :
s.sup (f ⊔ g) = s.sup f ⊔ s.sup g
source
theorem Finset.sup_congr {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s₁ s₂ : Finset β} {f g : β → α} (hs : s₁ = s₂) (hfg : ∀ a ∈ s₂, f a = g a) :
s₁.sup f = s₂.sup g
source
@[simp]
theorem map_finset_sup {F : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Type u_5} [SemilatticeSup α] [OrderBot α] [SemilatticeSup β] [OrderBot β] [FunLike F α β] [SupBotHomClass F α β] (f : F) (s : Finset ι) (g : ι → α) :
f (s.sup g) = s.sup (⇑f ∘ g)
source
@[simp]
theorem Finset.sup_le_iff {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} {f : β → α} {a : α} :
s.sup f ≤ a ↔ ∀ b ∈ s, f b ≤ a
source
theorem Finset.sup_le {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} {f : β → α} {a : α} :
(∀ b ∈ s, f b ≤ a) → s.sup f ≤ a

Alias of the reverse direction of `Finset.sup_le_iff`.

source
theorem Finset.sup_const_le {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} {a : α} :
(s.sup fun (x : β) => a) ≤ a
source
theorem Finset.le_sup {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} {f : β → α} {b : β} (hb : b ∈ s) :
f b ≤ s.sup f
source
theorem Finset.isLUB_sup {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} {f : β → α} :
IsLUB (f '' ↑s) (s.sup f)
source
theorem Finset.isLUB_sup_id {α : Type u_2} [SemilatticeSup α] [OrderBot α] {s : Finset α} :
IsLUB (↑s) (s.sup id)
source
theorem Finset.le_sup_of_le {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} {f : β → α} {a : α} {b : β} (hb : b ∈ s) (h : a ≤ f b) :
a ≤ s.sup f
source
theorem Finset.sup_union {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s₁ s₂ : Finset β} {f : β → α} [DecidableEq β] :
(s₁ ∪ s₂).sup f = s₁.sup f ⊔ s₂.sup f
source
theorem Finset.sup_const {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} (h : s.Nonempty) (c : α) :
(s.sup fun (x : β) => c) = c
source
@[simp]
theorem Finset.sup_bot {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] (s : Finset β) :
(s.sup fun (x : β) => ⊥) = ⊥
source
theorem Finset.sup_ite {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} {f g : β → α} (p : β → Prop) [DecidablePred p] :
(s.sup fun (i : β) => if p i then f i else g i) = (filter p s).sup f ⊔ {i ∈ s | ¬p i}.sup g
source
theorem Finset.sup_mono_fun {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} {f g : β → α} (h : ∀ b ∈ s, f b ≤ g b) :
s.sup f ≤ s.sup g
source
theorem Finset.sup_mono {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s₁ s₂ : Finset β} {f : β → α} (h : s₁ ⊆ s₂) :
s₁.sup f ≤ s₂.sup f
source
theorem Finset.sup_comm {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeSup α] [OrderBot α] (s : Finset β) (t : Finset γ) (f : β → γ → α) :
(s.sup fun (b : β) => t.sup (f b)) = t.sup fun (c : γ) => s.sup fun (b : β) => f b c
source
@[simp]
theorem Finset.sup_attach {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] (s : Finset β) (f : β → α) :
(s.attach.sup fun (x : { x : β // x ∈ s }) => f ↑x) = s.sup f
source
@[simp]
theorem Finset.sup_erase_bot {α : Type u_2} [SemilatticeSup α] [OrderBot α] [DecidableEq α] (s : Finset α) :
(s.erase ⊥).sup id = s.sup id
source
theorem Finset.sup_sdiff_right {α : Type u_7} {β : Type u_8} [GeneralizedBooleanAlgebra α] (s : Finset β) (f : β → α) (a : α) :
(s.sup fun (b : β) => f b \ a) = s.sup f \ a
source
theorem Finset.comp_sup_eq_sup_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeSup α] [OrderBot α] [SemilatticeSup γ] [OrderBot γ] {s : Finset β} {f : β → α} (g : α → γ) (g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y) (bot : g ⊥ = ⊥) :
g (s.sup f) = s.sup (g ∘ f)
source
theorem Finset.sup_coe {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {P : α → Prop} {Pbot : P ⊥} {Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)} (t : Finset β) (f : β → { x : α // P x }) :
↑(t.sup f) = t.sup fun (x : β) => ↑(f x)

Computing `sup` in a subtype (closed under `sup`) is the same as computing it in `α`.

source
@[simp]
theorem Finset.sup_toFinset {α : Type u_7} {β : Type u_8} [DecidableEq β] (s : Finset α) (f : α → Multiset β) :
(s.sup f).toFinset = s.sup fun (x : α) => (f x).toFinset
source
theorem List.foldr_sup_eq_sup_toFinset {α : Type u_2} [SemilatticeSup α] [OrderBot α] [DecidableEq α] (l : List α) :
foldr (fun (x1 x2 : α) => x1 ⊔ x2) ⊥ l = l.toFinset.sup id
source
theorem Finset.subset_range_sup_succ (s : Finset ℕ) :
s ⊆ range (s.sup id).succ
source
theorem Finset.sup_induction {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} {f : β → α} {p : α → Prop} (hb : p ⊥) (hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)) (hs : ∀ b ∈ s, p (f b)) :
p (s.sup f)
source
theorem Finset.sup_le_of_le_directed {α : Type u_7} [SemilatticeSup α] [OrderBot α] (s : Set α) (hs : s.Nonempty) (hdir : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) s) (t : Finset α) :
(∀ x ∈ t, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, t.sup id ≤ x
source
theorem Finset.sup_mem {α : Type u_2} [SemilatticeSup α] [OrderBot α] (s : Set α) (w₁ : ⊥ ∈ s) (w₂ : ∀ x ∈ s, ∀ y ∈ s, x ⊔ y ∈ s) {ι : Type u_7} (t : Finset ι) (p : ι → α) (h : ∀ i ∈ t, p i ∈ s) :
t.sup p ∈ s
source
@[simp]
theorem Finset.sup_eq_bot_iff {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] (f : β → α) (S : Finset β) :
S.sup f = ⊥ ↔ ∀ s ∈ S, f s = ⊥
source
@[simp]
theorem Finset.sup_disjSum {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeSup α] [OrderBot α] (s : Finset β) (t : Finset γ) (f : β ⊕ γ → α) :
(s.disjSum t).sup f = (s.sup fun (x : β) => f (Sum.inl x)) ⊔ t.sup fun (x : γ) => f (Sum.inr x)
source
@[simp]
theorem Finset.sup_eq_bot_of_isEmpty {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] [IsEmpty β] (f : β → α) (S : Finset β) :
S.sup f = ⊥
source
theorem Finset.le_sup_dite_pos {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} (p : β → Prop) [DecidablePred p] {f : (b : β) → p b → α} {g : (b : β) → ¬p b → α} {b : β} (h₀ : b ∈ s) (h₁ : p b) :
f b h₁ ≤ s.sup fun (i : β) => if h : p i then f i h else g i h
source
theorem Finset.le_sup_dite_neg {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} (p : β → Prop) [DecidablePred p] {f : (b : β) → p b → α} {g : (b : β) → ¬p b → α} {b : β} (h₀ : b ∈ s) (h₁ : ¬p b) :
g b h₁ ≤ s.sup fun (i : β) => if h : p i then f i h else g i h
source
theorem Finset.sup_eq_iSup {α : Type u_2} {β : Type u_3} [CompleteLattice β] (s : Finset α) (f : α → β) :
s.sup f = ⨆ a ∈ s, f a
source
theorem Finset.sup_id_eq_sSup {α : Type u_2} [CompleteLattice α] (s : Finset α) :
s.sup id = sSup ↑s
source
theorem Finset.sup_id_set_eq_sUnion {α : Type u_2} (s : Finset (Set α)) :
s.sup id = ⋃₀ ↑s
source
@[simp]
theorem Finset.sup_set_eq_biUnion {α : Type u_2} {β : Type u_3} (s : Finset α) (f : α → Set β) :
s.sup f = ⋃ x ∈ s, f x
source
theorem Finset.sup_eq_sSup_image {α : Type u_2} {β : Type u_3} [CompleteLattice β] (s : Finset α) (f : α → β) :
s.sup f = sSup (f '' ↑s)
source
theorem Finset.exists_sup_ge {α : Type u_2} {β : Type u_3} [SemilatticeSup β] [OrderBot β] [WellFoundedGT β] (f : α → β) :
∃ (t : Finset α), ∀ (a : α), f a ≤ t.sup f
source
theorem Finset.exists_sup_eq_iSup {α : Type u_2} {β : Type u_3} [CompleteLattice β] [WellFoundedGT β] (f : α → β) :
∃ (t : Finset α), t.sup f = ⨆ (a : α), f a

### inf #

source
def Finset.inf {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] (s : Finset β) (f : β → α) :
α

Infimum of a finite set: `inf {a, b, c} f = f a ⊓ f b ⊓ f c`

Equations

- s.inf f = Finset.fold (fun (x1 x2 : α) => x1 ⊓ x2) ⊤ f s

Instances For

source
theorem Finset.inf_def {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s : Finset β} {f : β → α} :
s.inf f = (Multiset.map f s.val).inf
source
@[simp]
theorem Finset.inf_empty {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {f : β → α} :
∅.inf f = ⊤
source
@[simp]
theorem Finset.inf_cons {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s : Finset β} {f : β → α} {b : β} (h : b ∉ s) :
(cons b s h).inf f = f b ⊓ s.inf f
source
@[simp]
theorem Finset.inf_insert {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s : Finset β} {f : β → α} [DecidableEq β] {b : β} :
(insert b s).inf f = f b ⊓ s.inf f
source
@[simp]
theorem Finset.inf_image {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeInf α] [OrderTop α] [DecidableEq β] (s : Finset γ) (f : γ → β) (g : β → α) :
(image f s).inf g = s.inf (g ∘ f)
source
@[simp]
theorem Finset.inf_map {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeInf α] [OrderTop α] (s : Finset γ) (f : γ ↪ β) (g : β → α) :
(map f s).inf g = s.inf (g ∘ ⇑f)
source
@[simp]
theorem Finset.inf_singleton {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {f : β → α} {b : β} :
{b}.inf f = f b
source
theorem Finset.inf_inf {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s : Finset β} {f g : β → α} :
s.inf (f ⊓ g) = s.inf f ⊓ s.inf g
source
theorem Finset.inf_congr {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s₁ s₂ : Finset β} {f g : β → α} (hs : s₁ = s₂) (hfg : ∀ a ∈ s₂, f a = g a) :
s₁.inf f = s₂.inf g
source
@[simp]
theorem map_finset_inf {F : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Type u_5} [SemilatticeInf α] [OrderTop α] [SemilatticeInf β] [OrderTop β] [FunLike F α β] [InfTopHomClass F α β] (f : F) (s : Finset ι) (g : ι → α) :
f (s.inf g) = s.inf (⇑f ∘ g)
source
@[simp]
theorem Finset.le_inf_iff {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s : Finset β} {f : β → α} {a : α} :
a ≤ s.inf f ↔ ∀ b ∈ s, a ≤ f b
source
theorem Finset.le_inf {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s : Finset β} {f : β → α} {a : α} :
(∀ b ∈ s, a ≤ f b) → a ≤ s.inf f

Alias of the reverse direction of `Finset.le_inf_iff`.

source
theorem Finset.le_inf_const_le {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s : Finset β} {a : α} :
a ≤ s.inf fun (x : β) => a
source
theorem Finset.inf_le {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s : Finset β} {f : β → α} {b : β} (hb : b ∈ s) :
s.inf f ≤ f b
source
theorem Finset.isGLB_inf {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s : Finset β} {f : β → α} :
IsGLB (f '' ↑s) (s.inf f)
source
theorem Finset.isGLB_inf_id {α : Type u_2} [SemilatticeInf α] [OrderTop α] {s : Finset α} :
IsGLB (↑s) (s.inf id)
source
theorem Finset.inf_le_of_le {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s : Finset β} {f : β → α} {a : α} {b : β} (hb : b ∈ s) (h : f b ≤ a) :
s.inf f ≤ a
source
theorem Finset.inf_union {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s₁ s₂ : Finset β} {f : β → α} [DecidableEq β] :
(s₁ ∪ s₂).inf f = s₁.inf f ⊓ s₂.inf f
source
theorem Finset.inf_const {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s : Finset β} (h : s.Nonempty) (c : α) :
(s.inf fun (x : β) => c) = c
source
@[simp]
theorem Finset.inf_top {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] (s : Finset β) :
(s.inf fun (x : β) => ⊤) = ⊤
source
theorem Finset.inf_ite {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s : Finset β} {f g : β → α} (p : β → Prop) [DecidablePred p] :
(s.inf fun (i : β) => if p i then f i else g i) = (filter p s).inf f ⊓ {i ∈ s | ¬p i}.inf g
source
theorem Finset.inf_mono_fun {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s : Finset β} {f g : β → α} (h : ∀ b ∈ s, f b ≤ g b) :
s.inf f ≤ s.inf g
source
theorem Finset.inf_mono {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s₁ s₂ : Finset β} {f : β → α} (h : s₁ ⊆ s₂) :
s₂.inf f ≤ s₁.inf f
source
theorem Finset.inf_comm {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeInf α] [OrderTop α] (s : Finset β) (t : Finset γ) (f : β → γ → α) :
(s.inf fun (b : β) => t.inf (f b)) = t.inf fun (c : γ) => s.inf fun (b : β) => f b c
source
theorem Finset.inf_attach {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] (s : Finset β) (f : β → α) :
(s.attach.inf fun (x : { x : β // x ∈ s }) => f ↑x) = s.inf f
source
@[simp]
theorem Finset.inf_erase_top {α : Type u_2} [SemilatticeInf α] [OrderTop α] [DecidableEq α] (s : Finset α) :
(s.erase ⊤).inf id = s.inf id
source
theorem Finset.comp_inf_eq_inf_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeInf α] [OrderTop α] [SemilatticeInf γ] [OrderTop γ] {s : Finset β} {f : β → α} (g : α → γ) (g_inf : ∀ (x y : α), g (x ⊓ y) = g x ⊓ g y) (top : g ⊤ = ⊤) :
g (s.inf f) = s.inf (g ∘ f)
source
theorem Finset.inf_coe {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {P : α → Prop} {Ptop : P ⊤} {Pinf : ∀ ⦃x y : α⦄, P x → P y → P (x ⊓ y)} (t : Finset β) (f : β → { x : α // P x }) :
↑(t.inf f) = t.inf fun (x : β) => ↑(f x)

Computing `inf` in a subtype (closed under `inf`) is the same as computing it in `α`.

source
theorem List.foldr_inf_eq_inf_toFinset {α : Type u_2} [SemilatticeInf α] [OrderTop α] [DecidableEq α] (l : List α) :
foldr (fun (x1 x2 : α) => x1 ⊓ x2) ⊤ l = l.toFinset.inf id
source
theorem Finset.inf_induction {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s : Finset β} {f : β → α} {p : α → Prop} (ht : p ⊤) (hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊓ a₂)) (hs : ∀ b ∈ s, p (f b)) :
p (s.inf f)
source
theorem Finset.inf_mem {α : Type u_2} [SemilatticeInf α] [OrderTop α] (s : Set α) (w₁ : ⊤ ∈ s) (w₂ : ∀ x ∈ s, ∀ y ∈ s, x ⊓ y ∈ s) {ι : Type u_7} (t : Finset ι) (p : ι → α) (h : ∀ i ∈ t, p i ∈ s) :
t.inf p ∈ s
source
@[simp]
theorem Finset.inf_eq_top_iff {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] (f : β → α) (S : Finset β) :
S.inf f = ⊤ ↔ ∀ s ∈ S, f s = ⊤
source
@[simp]
theorem Finset.inf_disjSum {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeInf α] [OrderTop α] (s : Finset β) (t : Finset γ) (f : β ⊕ γ → α) :
(s.disjSum t).inf f = (s.inf fun (x : β) => f (Sum.inl x)) ⊓ t.inf fun (x : γ) => f (Sum.inr x)
source
theorem Finset.inf_dite_pos_le {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s : Finset β} (p : β → Prop) [DecidablePred p] {f : (b : β) → p b → α} {g : (b : β) → ¬p b → α} {b : β} (h₀ : b ∈ s) (h₁ : p b) :
(s.inf fun (i : β) => if h : p i then f i h else g i h) ≤ f b h₁
source
theorem Finset.inf_dite_neg_le {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s : Finset β} (p : β → Prop) [DecidablePred p] {f : (b : β) → p b → α} {g : (b : β) → ¬p b → α} {b : β} (h₀ : b ∈ s) (h₁ : ¬p b) :
(s.inf fun (i : β) => if h : p i then f i h else g i h) ≤ g b h₁
source
@[simp]
theorem Finset.toDual_sup {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] (s : Finset β) (f : β → α) :
OrderDual.toDual (s.sup f) = s.inf (⇑OrderDual.toDual ∘ f)
source
@[simp]
theorem Finset.toDual_inf {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] (s : Finset β) (f : β → α) :
OrderDual.toDual (s.inf f) = s.sup (⇑OrderDual.toDual ∘ f)
source
@[simp]
theorem Finset.ofDual_sup {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] (s : Finset β) (f : β → α ᵒᵈ) :
OrderDual.ofDual (s.sup f) = s.inf (⇑OrderDual.ofDual ∘ f)
source
@[simp]
theorem Finset.ofDual_inf {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] (s : Finset β) (f : β → α ᵒᵈ) :
OrderDual.ofDual (s.inf f) = s.sup (⇑OrderDual.ofDual ∘ f)
source
theorem Finset.sup_inf_distrib_left {α : Type u_2} {ι : Type u_5} [DistribLattice α] [OrderBot α] (s : Finset ι) (f : ι → α) (a : α) :
a ⊓ s.sup f = s.sup fun (i : ι) => a ⊓ f i
source
theorem Finset.sup_inf_distrib_right {α : Type u_2} {ι : Type u_5} [DistribLattice α] [OrderBot α] (s : Finset ι) (f : ι → α) (a : α) :
s.sup f ⊓ a = s.sup fun (i : ι) => f i ⊓ a
source
theorem Finset.disjoint_sup_right {α : Type u_2} {ι : Type u_5} [DistribLattice α] [OrderBot α] {s : Finset ι} {f : ι → α} {a : α} :
Disjoint a (s.sup f) ↔ ∀ ⦃i : ι⦄, i ∈ s → Disjoint a (f i)
source
theorem Finset.disjoint_sup_left {α : Type u_2} {ι : Type u_5} [DistribLattice α] [OrderBot α] {s : Finset ι} {f : ι → α} {a : α} :
Disjoint (s.sup f) a ↔ ∀ ⦃i : ι⦄, i ∈ s → Disjoint (f i) a
source
theorem Finset.inf_sup_distrib_left {α : Type u_2} {ι : Type u_5} [DistribLattice α] [OrderTop α] (s : Finset ι) (f : ι → α) (a : α) :
a ⊔ s.inf f = s.inf fun (i : ι) => a ⊔ f i
source
theorem Finset.inf_sup_distrib_right {α : Type u_2} {ι : Type u_5} [DistribLattice α] [OrderTop α] (s : Finset ι) (f : ι → α) (a : α) :
s.inf f ⊔ a = s.inf fun (i : ι) => f i ⊔ a
source
theorem Finset.codisjoint_inf_right {α : Type u_2} {ι : Type u_5} [DistribLattice α] [OrderTop α] {f : ι → α} {s : Finset ι} {a : α} :
Codisjoint a (s.inf f) ↔ ∀ ⦃i : ι⦄, i ∈ s → Codisjoint a (f i)
source
theorem Finset.codisjoint_inf_left {α : Type u_2} {ι : Type u_5} [DistribLattice α] [OrderTop α] {f : ι → α} {s : Finset ι} {a : α} :
Codisjoint (s.inf f) a ↔ ∀ ⦃i : ι⦄, i ∈ s → Codisjoint (f i) a
source
theorem Finset.sup_sdiff_left {α : Type u_2} {ι : Type u_5} [BooleanAlgebra α] (s : Finset ι) (f : ι → α) (a : α) :
(s.sup fun (b : ι) => a \ f b) = a \ s.inf f
source
theorem Finset.inf_sdiff_left {α : Type u_2} {ι : Type u_5} [BooleanAlgebra α] {s : Finset ι} (hs : s.Nonempty) (f : ι → α) (a : α) :
(s.inf fun (b : ι) => a \ f b) = a \ s.sup f
source
theorem Finset.inf_sdiff_right {α : Type u_2} {ι : Type u_5} [BooleanAlgebra α] {s : Finset ι} (hs : s.Nonempty) (f : ι → α) (a : α) :
(s.inf fun (b : ι) => f b \ a) = s.inf f \ a
source
theorem Finset.inf_himp_right {α : Type u_2} {ι : Type u_5} [BooleanAlgebra α] (s : Finset ι) (f : ι → α) (a : α) :
(s.inf fun (b : ι) => f b ⇨ a) = s.sup f ⇨ a
source
theorem Finset.sup_himp_right {α : Type u_2} {ι : Type u_5} [BooleanAlgebra α] {s : Finset ι} (hs : s.Nonempty) (f : ι → α) (a : α) :
(s.sup fun (b : ι) => f b ⇨ a) = s.inf f ⇨ a
source
theorem Finset.sup_himp_left {α : Type u_2} {ι : Type u_5} [BooleanAlgebra α] {s : Finset ι} (hs : s.Nonempty) (f : ι → α) (a : α) :
(s.sup fun (b : ι) => a ⇨ f b) = a ⇨ s.sup f
source
@[simp]
theorem Finset.compl_sup {α : Type u_2} {ι : Type u_5} [BooleanAlgebra α] (s : Finset ι) (f : ι → α) :
(s.sup f)ᶜ = s.inf fun (i : ι) => (f i)ᶜ
source
@[simp]
theorem Finset.compl_inf {α : Type u_2} {ι : Type u_5} [BooleanAlgebra α] (s : Finset ι) (f : ι → α) :
(s.inf f)ᶜ = s.sup fun (i : ι) => (f i)ᶜ
source
theorem Finset.comp_sup_eq_sup_comp_of_is_total {α : Type u_2} {β : Type u_3} {ι : Type u_5} [LinearOrder α] [OrderBot α] {s : Finset ι} {f : ι → α} [SemilatticeSup β] [OrderBot β] (g : α → β) (mono_g : Monotone g) (bot : g ⊥ = ⊥) :
g (s.sup f) = s.sup (g ∘ f)
source
@[simp]
theorem Finset.le_sup_iff {α : Type u_2} {ι : Type u_5} [LinearOrder α] [OrderBot α] {s : Finset ι} {f : ι → α} {a : α} (ha : ⊥ < a) :
a ≤ s.sup f ↔ ∃ b ∈ s, a ≤ f b
source
theorem Finset.sup_eq_top_iff {ι : Type u_5} {α : Type u_7} [LinearOrder α] [BoundedOrder α] [Nontrivial α] {s : Finset ι} {f : ι → α} :
s.sup f = ⊤ ↔ ∃ b ∈ s, f b = ⊤
source
theorem Finset.Nonempty.sup_eq_top_iff {ι : Type u_5} {α : Type u_7} [LinearOrder α] [BoundedOrder α] {s : Finset ι} {f : ι → α} (hs : s.Nonempty) :
s.sup f = ⊤ ↔ ∃ b ∈ s, f b = ⊤
source
@[simp]
theorem Finset.lt_sup_iff {α : Type u_2} {ι : Type u_5} [LinearOrder α] [OrderBot α] {s : Finset ι} {f : ι → α} {a : α} :
a < s.sup f ↔ ∃ b ∈ s, a < f b
source
@[simp]
theorem Finset.sup_lt_iff {α : Type u_2} {ι : Type u_5} [LinearOrder α] [OrderBot α] {s : Finset ι} {f : ι → α} {a : α} (ha : ⊥ < a) :
s.sup f < a ↔ ∀ b ∈ s, f b < a
source
theorem Finset.sup_mem_of_nonempty {α : Type u_2} {ι : Type u_5} [LinearOrder α] [OrderBot α] {s : Finset ι} {f : ι → α} (hs : s.Nonempty) :
s.sup f ∈ f '' ↑s
source
theorem Finset.comp_inf_eq_inf_comp_of_is_total {α : Type u_2} {β : Type u_3} {ι : Type u_5} [LinearOrder α] [OrderTop α] {s : Finset ι} {f : ι → α} [SemilatticeInf β] [OrderTop β] (g : α → β) (mono_g : Monotone g) (top : g ⊤ = ⊤) :
g (s.inf f) = s.inf (g ∘ f)
source
@[simp]
theorem Finset.inf_le_iff {α : Type u_2} {ι : Type u_5} [LinearOrder α] [OrderTop α] {s : Finset ι} {f : ι → α} {a : α} (ha : a < ⊤) :
s.inf f ≤ a ↔ ∃ b ∈ s, f b ≤ a
source
theorem Finset.inf_eq_bot_iff {ι : Type u_5} {α : Type u_7} [LinearOrder α] [BoundedOrder α] [Nontrivial α] {s : Finset ι} {f : ι → α} :
s.inf f = ⊥ ↔ ∃ b ∈ s, f b = ⊥
source
theorem Finset.Nonempty.inf_eq_bot_iff {ι : Type u_5} {α : Type u_7} [LinearOrder α] [BoundedOrder α] {s : Finset ι} {f : ι → α} (h : s.Nonempty) :
s.inf f = ⊥ ↔ ∃ b ∈ s, f b = ⊥
source
@[simp]
theorem Finset.inf_lt_iff {α : Type u_2} {ι : Type u_5} [LinearOrder α] [OrderTop α] {s : Finset ι} {f : ι → α} {a : α} :
s.inf f < a ↔ ∃ b ∈ s, f b < a
source
@[simp]
theorem Finset.lt_inf_iff {α : Type u_2} {ι : Type u_5} [LinearOrder α] [OrderTop α] {s : Finset ι} {f : ι → α} {a : α} (ha : a < ⊤) :
a < s.inf f ↔ ∀ b ∈ s, a < f b
source
theorem Finset.inf_eq_iInf {α : Type u_2} {β : Type u_3} [CompleteLattice β] (s : Finset α) (f : α → β) :
s.inf f = ⨅ a ∈ s, f a
source
theorem Finset.inf_id_eq_sInf {α : Type u_2} [CompleteLattice α] (s : Finset α) :
s.inf id = sInf ↑s
source
theorem Finset.inf_id_set_eq_sInter {α : Type u_2} (s : Finset (Set α)) :
s.inf id = ⋂₀ ↑s
source
@[simp]
theorem Finset.inf_set_eq_iInter {α : Type u_2} {β : Type u_3} (s : Finset α) (f : α → Set β) :
s.inf f = ⋂ x ∈ s, f x
source
theorem Finset.inf_eq_sInf_image {α : Type u_2} {β : Type u_3} [CompleteLattice β] (s : Finset α) (f : α → β) :
s.inf f = sInf (f '' ↑s)
source
theorem Finset.exists_inf_le {α : Type u_2} {β : Type u_3} [SemilatticeInf β] [OrderTop β] [WellFoundedLT β] (f : α → β) :
∃ (t : Finset α), ∀ (a : α), t.inf f ≤ f a
source
theorem Finset.exists_inf_eq_iInf {α : Type u_2} {β : Type u_3} [CompleteLattice β] [WellFoundedLT β] (f : α → β) :
∃ (t : Finset α), t.inf f = ⨅ (a : α), f a
source
theorem Finset.sup_of_mem {α : Type u_2} {β : Type u_3} [SemilatticeSup α] {s : Finset β} (f : β → α) {b : β} (h : b ∈ s) :
∃ (a : α), s.sup (WithBot.some ∘ f) = ↑a
source
def Finset.sup' {α : Type u_2} {β : Type u_3} [SemilatticeSup α] (s : Finset β) (H : s.Nonempty) (f : β → α) :
α

Given nonempty finset `s` then `s.sup' H f` is the supremum of its image under `f` in (possibly unbounded) join-semilattice `α`, where `H` is a proof of nonemptiness. If `α` has a bottom element you may instead use `Finset.sup` which does not require `s` nonempty.

Equations

- s.sup' H f = (s.sup (WithBot.some ∘ f)).unbot ⋯

Instances For

source
@[simp]
theorem Finset.coe_sup' {α : Type u_2} {β : Type u_3} [SemilatticeSup α] {s : Finset β} (H : s.Nonempty) (f : β → α) :
↑(s.sup' H f) = s.sup (WithBot.some ∘ f)
source
@[simp]
theorem Finset.sup'_cons {α : Type u_2} {β : Type u_3} [SemilatticeSup α] {s : Finset β} (H : s.Nonempty) (f : β → α) {b : β} {hb : b ∉ s} :
(cons b s hb).sup' ⋯ f = f b ⊔ s.sup' H f
source
@[simp]
theorem Finset.sup'_insert {α : Type u_2} {β : Type u_3} [SemilatticeSup α] {s : Finset β} (H : s.Nonempty) (f : β → α) [DecidableEq β] {b : β} :
(insert b s).sup' ⋯ f = f b ⊔ s.sup' H f
source
@[simp]
theorem Finset.sup'_singleton {α : Type u_2} {β : Type u_3} [SemilatticeSup α] (f : β → α) {b : β} :
{b}.sup' ⋯ f = f b
source
@[simp]
theorem Finset.sup'_le_iff {α : Type u_2} {β : Type u_3} [SemilatticeSup α] {s : Finset β} (H : s.Nonempty) (f : β → α) {a : α} :
s.sup' H f ≤ a ↔ ∀ b ∈ s, f b ≤ a
source
theorem Finset.sup'_le {α : Type u_2} {β : Type u_3} [SemilatticeSup α] {s : Finset β} (H : s.Nonempty) (f : β → α) {a : α} :
(∀ b ∈ s, f b ≤ a) → s.sup' H f ≤ a

Alias of the reverse direction of `Finset.sup'_le_iff`.

source
theorem Finset.le_sup' {α : Type u_2} {β : Type u_3} [SemilatticeSup α] {s : Finset β} (f : β → α) {b : β} (h : b ∈ s) :
f b ≤ s.sup' ⋯ f
source
theorem Finset.isLUB_sup' {α : Type u_2} [SemilatticeSup α] {s : Finset α} (hs : s.Nonempty) :
IsLUB (↑s) (s.sup' hs id)
source
theorem Finset.le_sup'_of_le {α : Type u_2} {β : Type u_3} [SemilatticeSup α] {s : Finset β} (f : β → α) {a : α} {b : β} (hb : b ∈ s) (h : a ≤ f b) :
a ≤ s.sup' ⋯ f
source
theorem Finset.sup'_eq_of_forall {α : Type u_2} {β : Type u_3} [SemilatticeSup α] {s : Finset β} (H : s.Nonempty) (f : β → α) {a : α} (h : ∀ b ∈ s, f b = a) :
s.sup' H f = a
source
@[simp]
theorem Finset.sup'_const {α : Type u_2} {β : Type u_3} [SemilatticeSup α] {s : Finset β} (H : s.Nonempty) (a : α) :
(s.sup' H fun (x : β) => a) = a
source
theorem Finset.sup'_union {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [DecidableEq β] {s₁ s₂ : Finset β} (h₁ : s₁.Nonempty) (h₂ : s₂.Nonempty) (f : β → α) :
(s₁ ∪ s₂).sup' ⋯ f = s₁.sup' h₁ f ⊔ s₂.sup' h₂ f
source
theorem Finset.sup'_comm {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeSup α] {s : Finset β} {t : Finset γ} (hs : s.Nonempty) (ht : t.Nonempty) (f : β → γ → α) :
(s.sup' hs fun (b : β) => t.sup' ht (f b)) = t.sup' ht fun (c : γ) => s.sup' hs fun (b : β) => f b c
source
theorem Finset.sup'_induction {α : Type u_2} {β : Type u_3} [SemilatticeSup α] {s : Finset β} (H : s.Nonempty) (f : β → α) {p : α → Prop} (hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)) (hs : ∀ b ∈ s, p (f b)) :
p (s.sup' H f)
source
theorem Finset.sup'_mem {α : Type u_2} [SemilatticeSup α] (s : Set α) (w : ∀ x ∈ s, ∀ y ∈ s, x ⊔ y ∈ s) {ι : Type u_7} (t : Finset ι) (H : t.Nonempty) (p : ι → α) (h : ∀ i ∈ t, p i ∈ s) :
t.sup' H p ∈ s
source
theorem Finset.sup'_congr {α : Type u_2} {β : Type u_3} [SemilatticeSup α] {s : Finset β} (H : s.Nonempty) {t : Finset β} {f g : β → α} (h₁ : s = t) (h₂ : ∀ x ∈ s, f x = g x) :
s.sup' H f = t.sup' ⋯ g
source
theorem Finset.comp_sup'_eq_sup'_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeSup α] [SemilatticeSup γ] {s : Finset β} (H : s.Nonempty) {f : β → α} (g : α → γ) (g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y) :
g (s.sup' H f) = s.sup' H (g ∘ f)
source
@[simp]
theorem map_finset_sup' {F : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Type u_5} [SemilatticeSup α] [SemilatticeSup β] [FunLike F α β] [SupHomClass F α β] (f : F) {s : Finset ι} (hs : s.Nonempty) (g : ι → α) :
f (s.sup' hs g) = s.sup' hs (⇑f ∘ g)
source
@[simp]
theorem Finset.sup'_image {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeSup α] [DecidableEq β] {s : Finset γ} {f : γ → β} (hs : (image f s).Nonempty) (g : β → α) :
(image f s).sup' hs g = s.sup' ⋯ (g ∘ f)

To rewrite from right to left, use `Finset.sup'_comp_eq_image`.

source
theorem Finset.sup'_comp_eq_image {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeSup α] [DecidableEq β] {s : Finset γ} {f : γ → β} (hs : s.Nonempty) (g : β → α) :
s.sup' hs (g ∘ f) = (image f s).sup' ⋯ g

A version of `Finset.sup'_image` with LHS and RHS reversed. Also, this lemma assumes that `s` is nonempty instead of assuming that its image is nonempty.

source
@[simp]
theorem Finset.sup'_map {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeSup α] {s : Finset γ} {f : γ ↪ β} (g : β → α) (hs : (map f s).Nonempty) :
(map f s).sup' hs g = s.sup' ⋯ (g ∘ ⇑f)

To rewrite from right to left, use `Finset.sup'_comp_eq_map`.

source
theorem Finset.sup'_comp_eq_map {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeSup α] {s : Finset γ} {f : γ ↪ β} (g : β → α) (hs : s.Nonempty) :
s.sup' hs (g ∘ ⇑f) = (map f s).sup' ⋯ g

A version of `Finset.sup'_map` with LHS and RHS reversed. Also, this lemma assumes that `s` is nonempty instead of assuming that its image is nonempty.

source
theorem Finset.sup'_mono {α : Type u_2} {β : Type u_3} [SemilatticeSup α] (f : β → α) {s₁ s₂ : Finset β} (h : s₁ ⊆ s₂) (h₁ : s₁.Nonempty) :
s₁.sup' h₁ f ≤ s₂.sup' ⋯ f
source
theorem Finset.sup'_mono_fun {α : Type u_2} {β : Type u_3} [SemilatticeSup α] {s : Finset β} {hs : s.Nonempty} {f g : β → α} (h : ∀ b ∈ s, f b ≤ g b) :
s.sup' hs f ≤ s.sup' hs g
source
theorem Finset.inf_of_mem {α : Type u_2} {β : Type u_3} [SemilatticeInf α] {s : Finset β} (f : β → α) {b : β} (h : b ∈ s) :
∃ (a : α), s.inf (WithTop.some ∘ f) = ↑a
source
def Finset.inf' {α : Type u_2} {β : Type u_3} [SemilatticeInf α] (s : Finset β) (H : s.Nonempty) (f : β → α) :
α

Given nonempty finset `s` then `s.inf' H f` is the infimum of its image under `f` in (possibly unbounded) meet-semilattice `α`, where `H` is a proof of nonemptiness. If `α` has a top element you may instead use `Finset.inf` which does not require `s` nonempty.

Equations

- s.inf' H f = (s.inf (WithTop.some ∘ f)).untop ⋯

Instances For

source
@[simp]
theorem Finset.coe_inf' {α : Type u_2} {β : Type u_3} [SemilatticeInf α] {s : Finset β} (H : s.Nonempty) (f : β → α) :
↑(s.inf' H f) = s.inf (WithTop.some ∘ f)
source
@[simp]
theorem Finset.inf'_cons {α : Type u_2} {β : Type u_3} [SemilatticeInf α] {s : Finset β} (H : s.Nonempty) (f : β → α) {b : β} {hb : b ∉ s} :
(cons b s hb).inf' ⋯ f = f b ⊓ s.inf' H f
source
@[simp]
theorem Finset.inf'_insert {α : Type u_2} {β : Type u_3} [SemilatticeInf α] {s : Finset β} (H : s.Nonempty) (f : β → α) [DecidableEq β] {b : β} :
(insert b s).inf' ⋯ f = f b ⊓ s.inf' H f
source
@[simp]
theorem Finset.inf'_singleton {α : Type u_2} {β : Type u_3} [SemilatticeInf α] (f : β → α) {b : β} :
{b}.inf' ⋯ f = f b
source
@[simp]
theorem Finset.le_inf'_iff {α : Type u_2} {β : Type u_3} [SemilatticeInf α] {s : Finset β} (H : s.Nonempty) (f : β → α) {a : α} :
a ≤ s.inf' H f ↔ ∀ b ∈ s, a ≤ f b
source
theorem Finset.le_inf' {α : Type u_2} {β : Type u_3} [SemilatticeInf α] {s : Finset β} (H : s.Nonempty) (f : β → α) {a : α} (hs : ∀ b ∈ s, a ≤ f b) :
a ≤ s.inf' H f
source
theorem Finset.inf'_le {α : Type u_2} {β : Type u_3} [SemilatticeInf α] {s : Finset β} (f : β → α) {b : β} (h : b ∈ s) :
s.inf' ⋯ f ≤ f b
source
theorem Finset.isGLB_inf' {α : Type u_2} [SemilatticeInf α] {s : Finset α} (hs : s.Nonempty) :
IsGLB (↑s) (s.inf' hs id)
source
theorem Finset.inf'_le_of_le {α : Type u_2} {β : Type u_3} [SemilatticeInf α] {s : Finset β} (f : β → α) {a : α} {b : β} (hb : b ∈ s) (h : f b ≤ a) :
s.inf' ⋯ f ≤ a
source
theorem Finset.inf'_eq_of_forall {α : Type u_2} {β : Type u_3} [SemilatticeInf α] {s : Finset β} (H : s.Nonempty) (f : β → α) {a : α} (h : ∀ b ∈ s, f b = a) :
s.inf' H f = a
source
@[simp]
theorem Finset.inf'_const {α : Type u_2} {β : Type u_3} [SemilatticeInf α] {s : Finset β} (H : s.Nonempty) (a : α) :
(s.inf' H fun (x : β) => a) = a
source
theorem Finset.inf'_union {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [DecidableEq β] {s₁ s₂ : Finset β} (h₁ : s₁.Nonempty) (h₂ : s₂.Nonempty) (f : β → α) :
(s₁ ∪ s₂).inf' ⋯ f = s₁.inf' h₁ f ⊓ s₂.inf' h₂ f
source
theorem Finset.inf'_comm {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeInf α] {s : Finset β} {t : Finset γ} (hs : s.Nonempty) (ht : t.Nonempty) (f : β → γ → α) :
(s.inf' hs fun (b : β) => t.inf' ht (f b)) = t.inf' ht fun (c : γ) => s.inf' hs fun (b : β) => f b c
source
theorem Finset.comp_inf'_eq_inf'_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeInf α] [SemilatticeInf γ] {s : Finset β} (H : s.Nonempty) {f : β → α} (g : α → γ) (g_inf : ∀ (x y : α), g (x ⊓ y) = g x ⊓ g y) :
g (s.inf' H f) = s.inf' H (g ∘ f)
source
theorem Finset.inf'_induction {α : Type u_2} {β : Type u_3} [SemilatticeInf α] {s : Finset β} (H : s.Nonempty) (f : β → α) {p : α → Prop} (hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊓ a₂)) (hs : ∀ b ∈ s, p (f b)) :
p (s.inf' H f)
source
theorem Finset.inf'_mem {α : Type u_2} [SemilatticeInf α] (s : Set α) (w : ∀ x ∈ s, ∀ y ∈ s, x ⊓ y ∈ s) {ι : Type u_7} (t : Finset ι) (H : t.Nonempty) (p : ι → α) (h : ∀ i ∈ t, p i ∈ s) :
t.inf' H p ∈ s
source
theorem Finset.inf'_congr {α : Type u_2} {β : Type u_3} [SemilatticeInf α] {s : Finset β} (H : s.Nonempty) {t : Finset β} {f g : β → α} (h₁ : s = t) (h₂ : ∀ x ∈ s, f x = g x) :
s.inf' H f = t.inf' ⋯ g
source
@[simp]
theorem map_finset_inf' {F : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Type u_5} [SemilatticeInf α] [SemilatticeInf β] [FunLike F α β] [InfHomClass F α β] (f : F) {s : Finset ι} (hs : s.Nonempty) (g : ι → α) :
f (s.inf' hs g) = s.inf' hs (⇑f ∘ g)
source
@[simp]
theorem Finset.inf'_image {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeInf α] [DecidableEq β] {s : Finset γ} {f : γ → β} (hs : (image f s).Nonempty) (g : β → α) :
(image f s).inf' hs g = s.inf' ⋯ (g ∘ f)

To rewrite from right to left, use `Finset.inf'_comp_eq_image`.

source
theorem Finset.inf'_comp_eq_image {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeInf α] [DecidableEq β] {s : Finset γ} {f : γ → β} (hs : s.Nonempty) (g : β → α) :
s.inf' hs (g ∘ f) = (image f s).inf' ⋯ g

A version of `Finset.inf'_image` with LHS and RHS reversed. Also, this lemma assumes that `s` is nonempty instead of assuming that its image is nonempty.

source
@[simp]
theorem Finset.inf'_map {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeInf α] {s : Finset γ} {f : γ ↪ β} (g : β → α) (hs : (map f s).Nonempty) :
(map f s).inf' hs g = s.inf' ⋯ (g ∘ ⇑f)

To rewrite from right to left, use `Finset.inf'_comp_eq_map`.

source
theorem Finset.inf'_comp_eq_map {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeInf α] {s : Finset γ} {f : γ ↪ β} (g : β → α) (hs : s.Nonempty) :
s.inf' hs (g ∘ ⇑f) = (map f s).inf' ⋯ g

A version of `Finset.inf'_map` with LHS and RHS reversed. Also, this lemma assumes that `s` is nonempty instead of assuming that its image is nonempty.

source
theorem Finset.inf'_mono {α : Type u_2} {β : Type u_3} [SemilatticeInf α] (f : β → α) {s₁ s₂ : Finset β} (h : s₁ ⊆ s₂) (h₁ : s₁.Nonempty) :
s₂.inf' ⋯ f ≤ s₁.inf' h₁ f
source
theorem Finset.sup'_eq_sup {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} (H : s.Nonempty) (f : β → α) :
s.sup' H f = s.sup f
source
theorem Finset.coe_sup_of_nonempty {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} (h : s.Nonempty) (f : β → α) :
↑(s.sup f) = s.sup (WithBot.some ∘ f)
source
theorem Finset.inf'_eq_inf {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s : Finset β} (H : s.Nonempty) (f : β → α) :
s.inf' H f = s.inf f
source
theorem Finset.coe_inf_of_nonempty {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s : Finset β} (h : s.Nonempty) (f : β → α) :
↑(s.inf f) = s.inf (WithTop.some ∘ f)
source
@[simp]
theorem Finset.sup_apply {α : Type u_2} {β : Type u_3} {C : β → Type u_7} [(b : β) → SemilatticeSup (C b)] [(b : β) → OrderBot (C b)] (s : Finset α) (f : α → (b : β) → C b) (b : β) :
s.sup f b = s.sup fun (a : α) => f a b
source
@[simp]
theorem Finset.inf_apply {α : Type u_2} {β : Type u_3} {C : β → Type u_7} [(b : β) → SemilatticeInf (C b)] [(b : β) → OrderTop (C b)] (s : Finset α) (f : α → (b : β) → C b) (b : β) :
s.inf f b = s.inf fun (a : α) => f a b
source
@[simp]
theorem Finset.sup'_apply {α : Type u_2} {β : Type u_3} {C : β → Type u_7} [(b : β) → SemilatticeSup (C b)] {s : Finset α} (H : s.Nonempty) (f : α → (b : β) → C b) (b : β) :
s.sup' H f b = s.sup' H fun (a : α) => f a b
source
@[simp]
theorem Finset.inf'_apply {α : Type u_2} {β : Type u_3} {C : β → Type u_7} [(b : β) → SemilatticeInf (C b)] {s : Finset α} (H : s.Nonempty) (f : α → (b : β) → C b) (b : β) :
s.inf' H f b = s.inf' H fun (a : α) => f a b
source
@[simp]
theorem Finset.toDual_sup' {α : Type u_2} {ι : Type u_5} [SemilatticeSup α] {s : Finset ι} (hs : s.Nonempty) (f : ι → α) :
OrderDual.toDual (s.sup' hs f) = s.inf' hs (⇑OrderDual.toDual ∘ f)
source
@[simp]
theorem Finset.toDual_inf' {α : Type u_2} {ι : Type u_5} [SemilatticeInf α] {s : Finset ι} (hs : s.Nonempty) (f : ι → α) :
OrderDual.toDual (s.inf' hs f) = s.sup' hs (⇑OrderDual.toDual ∘ f)
source
@[simp]
theorem Finset.ofDual_sup' {α : Type u_2} {ι : Type u_5} [SemilatticeInf α] {s : Finset ι} (hs : s.Nonempty) (f : ι → α ᵒᵈ) :
OrderDual.ofDual (s.sup' hs f) = s.inf' hs (⇑OrderDual.ofDual ∘ f)
source
@[simp]
theorem Finset.ofDual_inf' {α : Type u_2} {ι : Type u_5} [SemilatticeSup α] {s : Finset ι} (hs : s.Nonempty) (f : ι → α ᵒᵈ) :
OrderDual.ofDual (s.inf' hs f) = s.sup' hs (⇑OrderDual.ofDual ∘ f)
source
theorem Finset.sup'_inf_distrib_left {α : Type u_2} {ι : Type u_5} [DistribLattice α] {s : Finset ι} (hs : s.Nonempty) (f : ι → α) (a : α) :
a ⊓ s.sup' hs f = s.sup' hs fun (i : ι) => a ⊓ f i
source
theorem Finset.sup'_inf_distrib_right {α : Type u_2} {ι : Type u_5} [DistribLattice α] {s : Finset ι} (hs : s.Nonempty) (f : ι → α) (a : α) :
s.sup' hs f ⊓ a = s.sup' hs fun (i : ι) => f i ⊓ a
source
theorem Finset.inf'_sup_distrib_left {α : Type u_2} {ι : Type u_5} [DistribLattice α] {s : Finset ι} (hs : s.Nonempty) (f : ι → α) (a : α) :
a ⊔ s.inf' hs f = s.inf' hs fun (i : ι) => a ⊔ f i
source
theorem Finset.inf'_sup_distrib_right {α : Type u_2} {ι : Type u_5} [DistribLattice α] {s : Finset ι} (hs : s.Nonempty) (f : ι → α) (a : α) :
s.inf' hs f ⊔ a = s.inf' hs fun (i : ι) => f i ⊔ a
source
theorem Finset.comp_sup_eq_sup_comp_of_nonempty {α : Type u_2} {β : Type u_3} {ι : Type u_5} [LinearOrder α] {s : Finset ι} {f : ι → α} [OrderBot α] [SemilatticeSup β] [OrderBot β] {g : α → β} (mono_g : Monotone g) (H : s.Nonempty) :
g (s.sup f) = s.sup (g ∘ f)
source
@[simp]
theorem Finset.le_sup'_iff {α : Type u_2} {ι : Type u_5} [LinearOrder α] {s : Finset ι} (H : s.Nonempty) {f : ι → α} {a : α} :
a ≤ s.sup' H f ↔ ∃ b ∈ s, a ≤ f b
source
@[simp]
theorem Finset.lt_sup'_iff {α : Type u_2} {ι : Type u_5} [LinearOrder α] {s : Finset ι} (H : s.Nonempty) {f : ι → α} {a : α} :
a < s.sup' H f ↔ ∃ b ∈ s, a < f b
source
@[simp]
theorem Finset.sup'_lt_iff {α : Type u_2} {ι : Type u_5} [LinearOrder α] {s : Finset ι} (H : s.Nonempty) {f : ι → α} {a : α} :
s.sup' H f < a ↔ ∀ i ∈ s, f i < a
source
@[simp]
theorem Finset.inf'_le_iff {α : Type u_2} {ι : Type u_5} [LinearOrder α] {s : Finset ι} (H : s.Nonempty) {f : ι → α} {a : α} :
s.inf' H f ≤ a ↔ ∃ i ∈ s, f i ≤ a
source
@[simp]
theorem Finset.inf'_lt_iff {α : Type u_2} {ι : Type u_5} [LinearOrder α] {s : Finset ι} (H : s.Nonempty) {f : ι → α} {a : α} :
s.inf' H f < a ↔ ∃ i ∈ s, f i < a
source
@[simp]
theorem Finset.lt_inf'_iff {α : Type u_2} {ι : Type u_5} [LinearOrder α] {s : Finset ι} (H : s.Nonempty) {f : ι → α} {a : α} :
a < s.inf' H f ↔ ∀ i ∈ s, a < f i
source
theorem Finset.exists_mem_eq_sup' {α : Type u_2} {ι : Type u_5} [LinearOrder α] {s : Finset ι} (H : s.Nonempty) (f : ι → α) :
∃ i ∈ s, s.sup' H f = f i
source
theorem Finset.exists_mem_eq_inf' {α : Type u_2} {ι : Type u_5} [LinearOrder α] {s : Finset ι} (H : s.Nonempty) (f : ι → α) :
∃ i ∈ s, s.inf' H f = f i
source
theorem Finset.exists_mem_eq_sup {α : Type u_2} {ι : Type u_5} [LinearOrder α] [OrderBot α] (s : Finset ι) (h : s.Nonempty) (f : ι → α) :
∃ i ∈ s, s.sup f = f i
source
theorem Finset.exists_mem_eq_inf {α : Type u_2} {ι : Type u_5} [LinearOrder α] [OrderTop α] (s : Finset ι) (h : s.Nonempty) (f : ι → α) :
∃ i ∈ s, s.inf f = f i
source
theorem Multiset.map_finset_sup {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq α] [DecidableEq β] (s : Finset γ) (f : γ → Multiset β) (g : β → α) (hg : Function.Injective g) :
map g (s.sup f) = s.sup (map g ∘ f)
source
theorem Multiset.count_finset_sup {α : Type u_2} {β : Type u_3} [DecidableEq β] (s : Finset α) (f : α → Multiset β) (b : β) :
count b (s.sup f) = s.sup fun (a : α) => count b (f a)
source
theorem Multiset.mem_sup {α : Type u_7} {β : Type u_8} [DecidableEq β] {s : Finset α} {f : α → Multiset β} {x : β} :
x ∈ s.sup f ↔ ∃ v ∈ s, x ∈ f v
source
@[simp]
theorem Finset.mem_sup' {α : Type u_2} {ι : Type u_5} [DecidableEq α] {s : Finset ι} {f : ι → Finset α} {a : α} (hs : s.Nonempty) :
a ∈ s.sup' hs f ↔ ∃ i ∈ s, a ∈ f i
source
@[simp]
theorem Finset.mem_inf' {α : Type u_2} {ι : Type u_5} [DecidableEq α] {s : Finset ι} {f : ι → Finset α} {a : α} (hs : s.Nonempty) :
a ∈ s.inf' hs f ↔ ∀ i ∈ s, a ∈ f i
source
@[simp]
theorem Finset.mem_sup {α : Type u_2} {ι : Type u_5} [DecidableEq α] {s : Finset ι} {f : ι → Finset α} {a : α} :
a ∈ s.sup f ↔ ∃ i ∈ s, a ∈ f i
source
@[simp]
theorem Finset.sup_singleton_apply {α : Type u_2} {β : Type u_3} [DecidableEq α] (s : Finset β) (f : β → α) :
(s.sup fun (b : β) => {f b}) = image f s
source
@[deprecated Finset.sup_singleton_apply (since := "2025-05-24")]
theorem Finset.sup_singleton'' {α : Type u_2} {β : Type u_3} [DecidableEq α] (s : Finset β) (f : β → α) :
(s.sup fun (b : β) => {f b}) = image f s

Alias of `Finset.sup_singleton_apply`.

source
@[simp]
theorem Finset.sup_singleton_eq_self {α : Type u_2} [DecidableEq α] (s : Finset α) :
s.sup singleton = s
source
@[deprecated Finset.sup_singleton_eq_self (since := "2025-05-24")]
theorem Finset.sup_singleton' {α : Type u_2} [DecidableEq α] (s : Finset α) :
s.sup singleton = s

Alias of `Finset.sup_singleton_eq_self`.