Documentation

Mathlib.Data.Finset.Lattice

Lattice operations on finsets #

sup #

def Finset.sup {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] [inst : OrderBot α] (s : Finset β) (f : βα) :
α

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

Equations
theorem Finset.sup_def {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] [inst : OrderBot α] {s : Finset β} {f : βα} :
@[simp]
theorem Finset.sup_empty {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] [inst : OrderBot α] {f : βα} :
@[simp]
theorem Finset.sup_cons {α : Type u_2} {β : Type u_1} [inst : SemilatticeSup α] [inst : OrderBot α] {s : Finset β} {f : βα} {b : β} (h : ¬b s) :
@[simp]
theorem Finset.sup_insert {α : Type u_2} {β : Type u_1} [inst : SemilatticeSup α] [inst : OrderBot α] {s : Finset β} {f : βα} [inst : DecidableEq β] {b : β} :
Finset.sup (insert b s) f = f b Finset.sup s f
theorem Finset.sup_image {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : SemilatticeSup α] [inst : OrderBot α] [inst : DecidableEq β] (s : Finset γ) (f : γβ) (g : βα) :
@[simp]
theorem Finset.sup_map {α : Type u_3} {β : Type u_2} {γ : Type u_1} [inst : SemilatticeSup α] [inst : OrderBot α] (s : Finset γ) (f : γ β) (g : βα) :
Finset.sup (Finset.map f s) g = Finset.sup s (g f)
@[simp]
theorem Finset.sup_singleton {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] [inst : OrderBot α] {f : βα} {b : β} :
Finset.sup {b} f = f b
theorem Finset.sup_union {α : Type u_2} {β : Type u_1} [inst : SemilatticeSup α] [inst : OrderBot α] {s₁ : Finset β} {s₂ : Finset β} {f : βα} [inst : DecidableEq β] :
Finset.sup (s₁ s₂) f = Finset.sup s₁ f Finset.sup s₂ f
theorem Finset.sup_sup {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] [inst : OrderBot α] {s : Finset β} {f : βα} {g : βα} :
theorem Finset.sup_congr {α : Type u_2} {β : Type u_1} [inst : SemilatticeSup α] [inst : OrderBot α] {s₁ : Finset β} {s₂ : Finset β} {f : βα} {g : βα} (hs : s₁ = s₂) (hfg : ∀ (a : β), a s₂f a = g a) :
Finset.sup s₁ f = Finset.sup s₂ g
@[simp]
theorem Finset.sup_le_iff {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] [inst : OrderBot α] {s : Finset β} {f : βα} {a : α} :
Finset.sup s f a ∀ (b : β), b sf b a
theorem Finset.sup_le {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] [inst : OrderBot α] {s : Finset β} {f : βα} {a : α} :
(∀ (b : β), b sf b a) → Finset.sup s f a

Alias of the reverse direction of Finset.sup_le_iff.

theorem Finset.sup_const_le {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] [inst : OrderBot α] {s : Finset β} {a : α} :
(Finset.sup s fun x => a) a
theorem Finset.le_sup {α : Type u_2} {β : Type u_1} [inst : SemilatticeSup α] [inst : OrderBot α] {s : Finset β} {f : βα} {b : β} (hb : b s) :
f b Finset.sup s f
@[simp]
theorem Finset.sup_bunionᵢ {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : SemilatticeSup α] [inst : OrderBot α] {f : βα} [inst : DecidableEq β] (s : Finset γ) (t : γFinset β) :
theorem Finset.sup_const {α : Type u_2} {β : Type u_1} [inst : SemilatticeSup α] [inst : OrderBot α] {s : Finset β} (h : Finset.Nonempty s) (c : α) :
(Finset.sup s fun x => c) = c
@[simp]
theorem Finset.sup_bot {α : Type u_2} {β : Type u_1} [inst : SemilatticeSup α] [inst : OrderBot α] (s : Finset β) :
(Finset.sup s fun x => ) =
theorem Finset.sup_ite {α : Type u_2} {β : Type u_1} [inst : SemilatticeSup α] [inst : OrderBot α] {s : Finset β} {f : βα} {g : βα} (p : βProp) [inst : DecidablePred p] :
(Finset.sup s fun i => if p i then f i else g i) = Finset.sup (Finset.filter p s) f Finset.sup (Finset.filter (fun i => ¬p i) s) g
theorem Finset.sup_mono_fun {α : Type u_2} {β : Type u_1} [inst : SemilatticeSup α] [inst : OrderBot α] {s : Finset β} {f : βα} {g : βα} (h : ∀ (b : β), b sf b g b) :
theorem Finset.sup_mono {α : Type u_2} {β : Type u_1} [inst : SemilatticeSup α] [inst : OrderBot α] {s₁ : Finset β} {s₂ : Finset β} {f : βα} (h : s₁ s₂) :
Finset.sup s₁ f Finset.sup s₂ f
theorem Finset.sup_comm {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : SemilatticeSup α] [inst : OrderBot α] (s : Finset β) (t : Finset γ) (f : βγα) :
(Finset.sup s fun b => Finset.sup t (f b)) = Finset.sup t fun c => Finset.sup s fun b => f b c
@[simp]
theorem Finset.sup_attach {α : Type u_2} {β : Type u_1} [inst : SemilatticeSup α] [inst : OrderBot α] (s : Finset β) (f : βα) :
(Finset.sup (Finset.attach s) fun x => f x) = Finset.sup s f
theorem Finset.sup_product_left {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : SemilatticeSup α] [inst : OrderBot α] (s : Finset β) (t : Finset γ) (f : β × γα) :
Finset.sup (s ×ᶠ t) f = Finset.sup s fun i => Finset.sup t fun i' => f (i, i')

See also Finset.product_bunionᵢ.

theorem Finset.sup_product_right {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : SemilatticeSup α] [inst : OrderBot α] (s : Finset β) (t : Finset γ) (f : β × γα) :
Finset.sup (s ×ᶠ t) f = Finset.sup t fun i' => Finset.sup s fun i => f (i, i')
@[simp]
theorem Finset.sup_erase_bot {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderBot α] [inst : DecidableEq α] (s : Finset α) :
theorem Finset.sup_sdiff_right {α : Type u_1} {β : Type u_2} [inst : GeneralizedBooleanAlgebra α] (s : Finset β) (f : βα) (a : α) :
(Finset.sup s fun b => f b \ a) = Finset.sup s f \ a
theorem Finset.comp_sup_eq_sup_comp {α : Type u_3} {β : Type u_2} {γ : Type u_1} [inst : SemilatticeSup α] [inst : OrderBot α] [inst : SemilatticeSup γ] [inst : OrderBot γ] {s : Finset β} {f : βα} (g : αγ) (g_sup : ∀ (x y : α), g (x y) = g x g y) (bot : g = ) :
g (Finset.sup s f) = Finset.sup s (g f)
theorem Finset.sup_coe {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] [inst : OrderBot α] {P : αProp} {Pbot : P } {Psup : x y : α⦄ → P xP yP (x y)} (t : Finset β) (f : β{ x // P x }) :
↑(Finset.sup t f) = Finset.sup t fun x => ↑(f x)

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

@[simp]
theorem Finset.sup_toFinset {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (s : Finset α) (f : αMultiset β) :
theorem List.foldr_sup_eq_sup_toFinset {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderBot α] [inst : DecidableEq α] (l : List α) :
List.foldr (fun x x_1 => x x_1) l = Finset.sup (List.toFinset l) id
theorem Finset.sup_induction {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] [inst : OrderBot α] {s : Finset β} {f : βα} {p : αProp} (hb : p ) (hp : (a₁ : α) → p a₁(a₂ : α) → p a₂p (a₁ a₂)) (hs : (b : β) → b sp (f b)) :
p (Finset.sup s f)
theorem Finset.sup_le_of_le_directed {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderBot α] (s : Set α) (hs : Set.Nonempty s) (hdir : DirectedOn (fun x x_1 => x x_1) s) (t : Finset α) :
(∀ (x : α), x ty, y s x y) → x, x s Finset.sup t id x
theorem Finset.sup_mem {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderBot α] (s : Set α) (w₁ : s) (w₂ : ∀ (x : α), x s∀ (y : α), y sx y s) {ι : Type u_2} (t : Finset ι) (p : ια) (h : ∀ (i : ι), i tp i s) :
@[simp]
theorem Finset.sup_eq_bot_iff {α : Type u_2} {β : Type u_1} [inst : SemilatticeSup α] [inst : OrderBot α] (f : βα) (S : Finset β) :
Finset.sup S f = ∀ (s : β), s Sf s =
theorem Finset.sup_eq_supᵢ {α : Type u_2} {β : Type u_1} [inst : CompleteLattice β] (s : Finset α) (f : αβ) :
Finset.sup s f = a, h, f a
theorem Finset.sup_id_eq_supₛ {α : Type u_1} [inst : CompleteLattice α] (s : Finset α) :
Finset.sup s id = supₛ s
theorem Finset.sup_id_set_eq_unionₛ {α : Type u_1} (s : Finset (Set α)) :
Finset.sup s id = ⋃₀ s
@[simp]
theorem Finset.sup_set_eq_bunionᵢ {α : Type u_1} {β : Type u_2} (s : Finset α) (f : αSet β) :
Finset.sup s f = Set.unionᵢ fun x => Set.unionᵢ fun h => f x
theorem Finset.sup_eq_supₛ_image {α : Type u_2} {β : Type u_1} [inst : CompleteLattice β] (s : Finset α) (f : αβ) :
Finset.sup s f = supₛ (f '' s)

inf #

def Finset.inf {α : Type u_1} {β : Type u_2} [inst : SemilatticeInf α] [inst : OrderTop α] (s : Finset β) (f : βα) :
α

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

Equations
theorem Finset.inf_def {α : Type u_1} {β : Type u_2} [inst : SemilatticeInf α] [inst : OrderTop α] {s : Finset β} {f : βα} :
@[simp]
theorem Finset.inf_empty {α : Type u_1} {β : Type u_2} [inst : SemilatticeInf α] [inst : OrderTop α] {f : βα} :
@[simp]
theorem Finset.inf_cons {α : Type u_2} {β : Type u_1} [inst : SemilatticeInf α] [inst : OrderTop α] {s : Finset β} {f : βα} {b : β} (h : ¬b s) :
@[simp]
theorem Finset.inf_insert {α : Type u_2} {β : Type u_1} [inst : SemilatticeInf α] [inst : OrderTop α] {s : Finset β} {f : βα} [inst : DecidableEq β] {b : β} :
Finset.inf (insert b s) f = f b Finset.inf s f
theorem Finset.inf_image {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : SemilatticeInf α] [inst : OrderTop α] [inst : DecidableEq β] (s : Finset γ) (f : γβ) (g : βα) :
@[simp]
theorem Finset.inf_map {α : Type u_3} {β : Type u_2} {γ : Type u_1} [inst : SemilatticeInf α] [inst : OrderTop α] (s : Finset γ) (f : γ β) (g : βα) :
Finset.inf (Finset.map f s) g = Finset.inf s (g f)
@[simp]
theorem Finset.inf_singleton {α : Type u_1} {β : Type u_2} [inst : SemilatticeInf α] [inst : OrderTop α] {f : βα} {b : β} :
Finset.inf {b} f = f b
theorem Finset.inf_union {α : Type u_2} {β : Type u_1} [inst : SemilatticeInf α] [inst : OrderTop α] {s₁ : Finset β} {s₂ : Finset β} {f : βα} [inst : DecidableEq β] :
Finset.inf (s₁ s₂) f = Finset.inf s₁ f Finset.inf s₂ f
theorem Finset.inf_inf {α : Type u_1} {β : Type u_2} [inst : SemilatticeInf α] [inst : OrderTop α] {s : Finset β} {f : βα} {g : βα} :
theorem Finset.inf_congr {α : Type u_2} {β : Type u_1} [inst : SemilatticeInf α] [inst : OrderTop α] {s₁ : Finset β} {s₂ : Finset β} {f : βα} {g : βα} (hs : s₁ = s₂) (hfg : ∀ (a : β), a s₂f a = g a) :
Finset.inf s₁ f = Finset.inf s₂ g
@[simp]
theorem Finset.inf_bunionᵢ {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : SemilatticeInf α] [inst : OrderTop α] {f : βα} [inst : DecidableEq β] (s : Finset γ) (t : γFinset β) :
theorem Finset.inf_const {α : Type u_2} {β : Type u_1} [inst : SemilatticeInf α] [inst : OrderTop α] {s : Finset β} (h : Finset.Nonempty s) (c : α) :
(Finset.inf s fun x => c) = c
@[simp]
theorem Finset.inf_top {α : Type u_2} {β : Type u_1} [inst : SemilatticeInf α] [inst : OrderTop α] (s : Finset β) :
(Finset.inf s fun x => ) =
theorem Finset.le_inf_iff {α : Type u_1} {β : Type u_2} [inst : SemilatticeInf α] [inst : OrderTop α] {s : Finset β} {f : βα} {a : α} :
a Finset.inf s f ∀ (b : β), b sa f b
theorem Finset.le_inf {α : Type u_1} {β : Type u_2} [inst : SemilatticeInf α] [inst : OrderTop α] {s : Finset β} {f : βα} {a : α} :
(∀ (b : β), b sa f b) → a Finset.inf s f

Alias of the reverse direction of Finset.le_inf_iff.

theorem Finset.le_inf_const_le {α : Type u_1} {β : Type u_2} [inst : SemilatticeInf α] [inst : OrderTop α] {s : Finset β} {a : α} :
a Finset.inf s fun x => a
theorem Finset.inf_le {α : Type u_2} {β : Type u_1} [inst : SemilatticeInf α] [inst : OrderTop α] {s : Finset β} {f : βα} {b : β} (hb : b s) :
Finset.inf s f f b
theorem Finset.inf_mono_fun {α : Type u_2} {β : Type u_1} [inst : SemilatticeInf α] [inst : OrderTop α] {s : Finset β} {f : βα} {g : βα} (h : ∀ (b : β), b sf b g b) :
theorem Finset.inf_mono {α : Type u_2} {β : Type u_1} [inst : SemilatticeInf α] [inst : OrderTop α] {s₁ : Finset β} {s₂ : Finset β} {f : βα} (h : s₁ s₂) :
Finset.inf s₂ f Finset.inf s₁ f
theorem Finset.inf_attach {α : Type u_2} {β : Type u_1} [inst : SemilatticeInf α] [inst : OrderTop α] (s : Finset β) (f : βα) :
(Finset.inf (Finset.attach s) fun x => f x) = Finset.inf s f
theorem Finset.inf_comm {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : SemilatticeInf α] [inst : OrderTop α] (s : Finset β) (t : Finset γ) (f : βγα) :
(Finset.inf s fun b => Finset.inf t (f b)) = Finset.inf t fun c => Finset.inf s fun b => f b c
theorem Finset.inf_product_left {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : SemilatticeInf α] [inst : OrderTop α] (s : Finset β) (t : Finset γ) (f : β × γα) :
Finset.inf (s ×ᶠ t) f = Finset.inf s fun i => Finset.inf t fun i' => f (i, i')
theorem Finset.inf_product_right {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : SemilatticeInf α] [inst : OrderTop α] (s : Finset β) (t : Finset γ) (f : β × γα) :
Finset.inf (s ×ᶠ t) f = Finset.inf t fun i' => Finset.inf s fun i => f (i, i')
@[simp]
theorem Finset.inf_erase_top {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderTop α] [inst : DecidableEq α] (s : Finset α) :
theorem Finset.sup_sdiff_left {α : Type u_1} {β : Type u_2} [inst : BooleanAlgebra α] (s : Finset β) (f : βα) (a : α) :
(Finset.sup s fun b => a \ f b) = a \ Finset.inf s f
theorem Finset.inf_sdiff_left {α : Type u_1} {β : Type u_2} [inst : BooleanAlgebra α] {s : Finset β} (hs : Finset.Nonempty s) (f : βα) (a : α) :
(Finset.inf s fun b => a \ f b) = a \ Finset.sup s f
theorem Finset.inf_sdiff_right {α : Type u_1} {β : Type u_2} [inst : BooleanAlgebra α] {s : Finset β} (hs : Finset.Nonempty s) (f : βα) (a : α) :
(Finset.inf s fun b => f b \ a) = Finset.inf s f \ a
theorem Finset.comp_inf_eq_inf_comp {α : Type u_3} {β : Type u_2} {γ : Type u_1} [inst : SemilatticeInf α] [inst : OrderTop α] [inst : SemilatticeInf γ] [inst : OrderTop γ] {s : Finset β} {f : βα} (g : αγ) (g_inf : ∀ (x y : α), g (x y) = g x g y) (top : g = ) :
g (Finset.inf s f) = Finset.inf s (g f)
theorem Finset.inf_coe {α : Type u_1} {β : Type u_2} [inst : SemilatticeInf α] [inst : OrderTop α] {P : αProp} {Ptop : P } {Pinf : x y : α⦄ → P xP yP (x y)} (t : Finset β) (f : β{ x // P x }) :
↑(Finset.inf t f) = Finset.inf t fun x => ↑(f x)

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

theorem List.foldr_inf_eq_inf_toFinset {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderTop α] [inst : DecidableEq α] (l : List α) :
List.foldr (fun x x_1 => x x_1) l = Finset.inf (List.toFinset l) id
theorem Finset.inf_induction {α : Type u_1} {β : Type u_2} [inst : SemilatticeInf α] [inst : OrderTop α] {s : Finset β} {f : βα} {p : αProp} (ht : p ) (hp : (a₁ : α) → p a₁(a₂ : α) → p a₂p (a₁ a₂)) (hs : (b : β) → b sp (f b)) :
p (Finset.inf s f)
theorem Finset.inf_mem {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderTop α] (s : Set α) (w₁ : s) (w₂ : ∀ (x : α), x s∀ (y : α), y sx y s) {ι : Type u_2} (t : Finset ι) (p : ια) (h : ∀ (i : ι), i tp i s) :
@[simp]
theorem Finset.inf_eq_top_iff {α : Type u_2} {β : Type u_1} [inst : SemilatticeInf α] [inst : OrderTop α] (f : βα) (S : Finset β) :
Finset.inf S f = ∀ (s : β), s Sf s =
@[simp]
theorem Finset.toDual_sup {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] [inst : OrderBot α] (s : Finset β) (f : βα) :
OrderDual.toDual (Finset.sup s f) = Finset.inf s (OrderDual.toDual f)
@[simp]
theorem Finset.toDual_inf {α : Type u_1} {β : Type u_2} [inst : SemilatticeInf α] [inst : OrderTop α] (s : Finset β) (f : βα) :
OrderDual.toDual (Finset.inf s f) = Finset.sup s (OrderDual.toDual f)
@[simp]
theorem Finset.ofDual_sup {α : Type u_1} {β : Type u_2} [inst : SemilatticeInf α] [inst : OrderTop α] (s : Finset β) (f : βαᵒᵈ) :
OrderDual.ofDual (Finset.sup s f) = Finset.inf s (OrderDual.ofDual f)
@[simp]
theorem Finset.ofDual_inf {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] [inst : OrderBot α] (s : Finset β) (f : βαᵒᵈ) :
OrderDual.ofDual (Finset.inf s f) = Finset.sup s (OrderDual.ofDual f)
theorem Finset.sup_inf_distrib_left {α : Type u_2} {ι : Type u_1} [inst : DistribLattice α] [inst : OrderBot α] (s : Finset ι) (f : ια) (a : α) :
a Finset.sup s f = Finset.sup s fun i => a f i
theorem Finset.sup_inf_distrib_right {α : Type u_2} {ι : Type u_1} [inst : DistribLattice α] [inst : OrderBot α] (s : Finset ι) (f : ια) (a : α) :
Finset.sup s f a = Finset.sup s fun i => f i a
theorem Finset.disjoint_sup_right {α : Type u_1} {β : Type u_2} [inst : DistribLattice α] [inst : OrderBot α] {s : Finset β} {f : βα} {a : α} :
Disjoint a (Finset.sup s f) ∀ (i : β), i sDisjoint a (f i)
theorem Finset.disjoint_sup_left {α : Type u_1} {β : Type u_2} [inst : DistribLattice α] [inst : OrderBot α] {s : Finset β} {f : βα} {a : α} :
Disjoint (Finset.sup s f) a ∀ (i : β), i sDisjoint (f i) a
theorem Finset.inf_sup_distrib_left {α : Type u_2} {ι : Type u_1} [inst : DistribLattice α] [inst : OrderTop α] (s : Finset ι) (f : ια) (a : α) :
a Finset.inf s f = Finset.inf s fun i => a f i
theorem Finset.inf_sup_distrib_right {α : Type u_2} {ι : Type u_1} [inst : DistribLattice α] [inst : OrderTop α] (s : Finset ι) (f : ια) (a : α) :
Finset.inf s f a = Finset.inf s fun i => f i a
theorem Finset.comp_sup_eq_sup_comp_of_is_total {α : Type u_2} {β : Type u_1} {ι : Type u_3} [inst : LinearOrder α] [inst : OrderBot α] {s : Finset ι} {f : ια} [inst : SemilatticeSup β] [inst : OrderBot β] (g : αβ) (mono_g : Monotone g) (bot : g = ) :
g (Finset.sup s f) = Finset.sup s (g f)
@[simp]
theorem Finset.le_sup_iff {α : Type u_1} {ι : Type u_2} [inst : LinearOrder α] [inst : OrderBot α] {s : Finset ι} {f : ια} {a : α} (ha : < a) :
a Finset.sup s f b, b s a f b
@[simp]
theorem Finset.lt_sup_iff {α : Type u_1} {ι : Type u_2} [inst : LinearOrder α] [inst : OrderBot α] {s : Finset ι} {f : ια} {a : α} :
a < Finset.sup s f b, b s a < f b
@[simp]
theorem Finset.sup_lt_iff {α : Type u_1} {ι : Type u_2} [inst : LinearOrder α] [inst : OrderBot α] {s : Finset ι} {f : ια} {a : α} (ha : < a) :
Finset.sup s f < a ∀ (b : ι), b sf b < a
theorem Finset.comp_inf_eq_inf_comp_of_is_total {α : Type u_2} {β : Type u_1} {ι : Type u_3} [inst : LinearOrder α] [inst : OrderTop α] {s : Finset ι} {f : ια} [inst : SemilatticeInf β] [inst : OrderTop β] (g : αβ) (mono_g : Monotone g) (top : g = ) :
g (Finset.inf s f) = Finset.inf s (g f)
@[simp]
theorem Finset.inf_le_iff {α : Type u_1} {ι : Type u_2} [inst : LinearOrder α] [inst : OrderTop α] {s : Finset ι} {f : ια} {a : α} (ha : a < ) :
Finset.inf s f a b, b s f b a
@[simp]
theorem Finset.inf_lt_iff {α : Type u_1} {ι : Type u_2} [inst : LinearOrder α] [inst : OrderTop α] {s : Finset ι} {f : ια} {a : α} :
Finset.inf s f < a b, b s f b < a
@[simp]
theorem Finset.lt_inf_iff {α : Type u_1} {ι : Type u_2} [inst : LinearOrder α] [inst : OrderTop α] {s : Finset ι} {f : ια} {a : α} (ha : a < ) :
a < Finset.inf s f ∀ (b : ι), b sa < f b
theorem Finset.inf_eq_infᵢ {α : Type u_2} {β : Type u_1} [inst : CompleteLattice β] (s : Finset α) (f : αβ) :
Finset.inf s f = a, h, f a
theorem Finset.inf_id_eq_infₛ {α : Type u_1} [inst : CompleteLattice α] (s : Finset α) :
Finset.inf s id = infₛ s
theorem Finset.inf_id_set_eq_interₛ {α : Type u_1} (s : Finset (Set α)) :
Finset.inf s id = ⋂₀ s
@[simp]
theorem Finset.inf_set_eq_interᵢ {α : Type u_1} {β : Type u_2} (s : Finset α) (f : αSet β) :
Finset.inf s f = Set.interᵢ fun x => Set.interᵢ fun h => f x
theorem Finset.inf_eq_infₛ_image {α : Type u_2} {β : Type u_1} [inst : CompleteLattice β] (s : Finset α) (f : αβ) :
Finset.inf s f = infₛ (f '' s)
theorem Finset.sup_of_mem {α : Type u_2} {β : Type u_1} [inst : SemilatticeSup α] {s : Finset β} (f : βα) {b : β} (h : b s) :
a, Finset.sup s (WithBot.some f) = a
def Finset.sup' {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] (s : Finset β) (H : Finset.Nonempty s) (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
@[simp]
theorem Finset.coe_sup' {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] {s : Finset β} (H : Finset.Nonempty s) (f : βα) :
↑(Finset.sup' s H f) = Finset.sup s (WithBot.some f)
@[simp]
theorem Finset.sup'_cons {α : Type u_2} {β : Type u_1} [inst : SemilatticeSup α] {s : Finset β} (H : Finset.Nonempty s) (f : βα) {b : β} {hb : ¬b s} {h : Finset.Nonempty (Finset.cons b s hb)} :
Finset.sup' (Finset.cons b s hb) h f = f b Finset.sup' s H f
@[simp]
theorem Finset.sup'_insert {α : Type u_2} {β : Type u_1} [inst : SemilatticeSup α] {s : Finset β} (H : Finset.Nonempty s) (f : βα) [inst : DecidableEq β] {b : β} {h : Finset.Nonempty (insert b s)} :
Finset.sup' (insert b s) h f = f b Finset.sup' s H f
@[simp]
theorem Finset.sup'_singleton {α : Type u_2} {β : Type u_1} [inst : SemilatticeSup α] (f : βα) {b : β} {h : Finset.Nonempty {b}} :
Finset.sup' {b} h f = f b
theorem Finset.sup'_le {α : Type u_2} {β : Type u_1} [inst : SemilatticeSup α] {s : Finset β} (H : Finset.Nonempty s) (f : βα) {a : α} (hs : ∀ (b : β), b sf b a) :
theorem Finset.le_sup' {α : Type u_2} {β : Type u_1} [inst : SemilatticeSup α] {s : Finset β} (f : βα) {b : β} (h : b s) :
f b Finset.sup' s (_ : x, x s) f
@[simp]
theorem Finset.sup'_const {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] {s : Finset β} (H : Finset.Nonempty s) (a : α) :
(Finset.sup' s H fun x => a) = a
@[simp]
theorem Finset.sup'_le_iff {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] {s : Finset β} (H : Finset.Nonempty s) (f : βα) {a : α} :
Finset.sup' s H f a ∀ (b : β), b sf b a
theorem Finset.sup'_bunionᵢ {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : SemilatticeSup α] (f : βα) [inst : DecidableEq β] {s : Finset γ} (Hs : Finset.Nonempty s) {t : γFinset β} (Ht : ∀ (b : γ), Finset.Nonempty (t b)) :
Finset.sup' (Finset.bunionᵢ s t) (_ : Finset.Nonempty (Finset.bunionᵢ s t)) f = Finset.sup' s Hs fun b => Finset.sup' (t b) (Ht b) f
theorem Finset.comp_sup'_eq_sup'_comp {α : Type u_3} {β : Type u_2} {γ : Type u_1} [inst : SemilatticeSup α] [inst : SemilatticeSup γ] {s : Finset β} (H : Finset.Nonempty s) {f : βα} (g : αγ) (g_sup : ∀ (x y : α), g (x y) = g x g y) :
g (Finset.sup' s H f) = Finset.sup' s H (g f)
theorem Finset.sup'_induction {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] {s : Finset β} (H : Finset.Nonempty s) (f : βα) {p : αProp} (hp : (a₁ : α) → p a₁(a₂ : α) → p a₂p (a₁ a₂)) (hs : (b : β) → b sp (f b)) :
p (Finset.sup' s H f)
theorem Finset.sup'_mem {α : Type u_1} [inst : SemilatticeSup α] (s : Set α) (w : ∀ (x : α), x s∀ (y : α), y sx y s) {ι : Type u_2} (t : Finset ι) (H : Finset.Nonempty t) (p : ια) (h : ∀ (i : ι), i tp i s) :
theorem Finset.sup'_congr {α : Type u_2} {β : Type u_1} [inst : SemilatticeSup α] {s : Finset β} (H : Finset.Nonempty s) {t : Finset β} {f : βα} {g : βα} (h₁ : s = t) (h₂ : ∀ (x : β), x sf x = g x) :
@[simp]
theorem Finset.sup'_map {α : Type u_3} {β : Type u_2} {γ : Type u_1} [inst : SemilatticeSup α] {s : Finset γ} {f : γ β} (g : βα) (hs : Finset.Nonempty (Finset.map f s)) (hs' : optParam (Finset.Nonempty s) (_ : Finset.Nonempty s)) :
Finset.sup' (Finset.map f s) hs g = Finset.sup' s hs' (g f)
theorem Finset.inf_of_mem {α : Type u_2} {β : Type u_1} [inst : SemilatticeInf α] {s : Finset β} (f : βα) {b : β} (h : b s) :
a, Finset.inf s (WithTop.some f) = a
def Finset.inf' {α : Type u_1} {β : Type u_2} [inst : SemilatticeInf α] (s : Finset β) (H : Finset.Nonempty s) (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
@[simp]
theorem Finset.coe_inf' {α : Type u_1} {β : Type u_2} [inst : SemilatticeInf α] {s : Finset β} (H : Finset.Nonempty s) (f : βα) :
↑(Finset.inf' s H f) = Finset.inf s (WithTop.some f)
@[simp]
theorem Finset.inf'_cons {α : Type u_2} {β : Type u_1} [inst : SemilatticeInf α] {s : Finset β} (H : Finset.Nonempty s) (f : βα) {b : β} {hb : ¬b s} {h : Finset.Nonempty (Finset.cons b s hb)} :
Finset.inf' (Finset.cons b s hb) h f = f b Finset.inf' s H f
@[simp]
theorem Finset.inf'_insert {α : Type u_2} {β : Type u_1} [inst : SemilatticeInf α] {s : Finset β} (H : Finset.Nonempty s) (f : βα) [inst : DecidableEq β] {b : β} {h : Finset.Nonempty (insert b s)} :
Finset.inf' (insert b s) h f = f b Finset.inf' s H f
@[simp]
theorem Finset.inf'_singleton {α : Type u_2} {β : Type u_1} [inst : SemilatticeInf α] (f : βα) {b : β} {h : Finset.Nonempty {b}} :
Finset.inf' {b} h f = f b
theorem Finset.le_inf' {α : Type u_2} {β : Type u_1} [inst : SemilatticeInf α] {s : Finset β} (H : Finset.Nonempty s) (f : βα) {a : α} (hs : ∀ (b : β), b sa f b) :
theorem Finset.inf'_le {α : Type u_2} {β : Type u_1} [inst : SemilatticeInf α] {s : Finset β} (f : βα) {b : β} (h : b s) :
Finset.inf' s (_ : x, x s) f f b
@[simp]
theorem Finset.inf'_const {α : Type u_1} {β : Type u_2} [inst : SemilatticeInf α] {s : Finset β} (H : Finset.Nonempty s) (a : α) :
(Finset.inf' s H fun x => a) = a
@[simp]
theorem Finset.le_inf'_iff {α : Type u_1} {β : Type u_2} [inst : SemilatticeInf α] {s : Finset β} (H : Finset.Nonempty s) (f : βα) {a : α} :
a Finset.inf' s H f ∀ (b : β), b sa f b
theorem Finset.inf'_bunionᵢ {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : SemilatticeInf α] (f : βα) [inst : DecidableEq β] {s : Finset γ} (Hs : Finset.Nonempty s) {t : γFinset β} (Ht : ∀ (b : γ), Finset.Nonempty (t b)) :
Finset.inf' (Finset.bunionᵢ s t) (_ : Finset.Nonempty (Finset.bunionᵢ s t)) f = Finset.inf' s Hs fun b => Finset.inf' (t b) (Ht b) f
theorem Finset.comp_inf'_eq_inf'_comp {α : Type u_3} {β : Type u_2} {γ : Type u_1} [inst : SemilatticeInf α] [inst : SemilatticeInf γ] {s : Finset β} (H : Finset.Nonempty s) {f : βα} (g : αγ) (g_inf : ∀ (x y : α), g (x y) = g x g y) :
g (Finset.inf' s H f) = Finset.inf' s H (g f)
theorem Finset.inf'_induction {α : Type u_1} {β : Type u_2} [inst : SemilatticeInf α] {s : Finset β} (H : Finset.Nonempty s) (f : βα) {p : αProp} (hp : (a₁ : α) → p a₁(a₂ : α) → p a₂p (a₁ a₂)) (hs : (b : β) → b sp (f b)) :
p (Finset.inf' s H f)
theorem Finset.inf'_mem {α : Type u_1} [inst : SemilatticeInf α] (s : Set α) (w : ∀ (x : α), x s∀ (y : α), y sx y s) {ι : Type u_2} (t : Finset ι) (H : Finset.Nonempty t) (p : ια) (h : ∀ (i : ι), i tp i s) :
theorem Finset.inf'_congr {α : Type u_2} {β : Type u_1} [inst : SemilatticeInf α] {s : Finset β} (H : Finset.Nonempty s) {t : Finset β} {f : βα} {g : βα} (h₁ : s = t) (h₂ : ∀ (x : β), x sf x = g x) :
@[simp]
theorem Finset.inf'_map {α : Type u_3} {β : Type u_2} {γ : Type u_1} [inst : SemilatticeInf α] {s : Finset γ} {f : γ β} (g : βα) (hs : Finset.Nonempty (Finset.map f s)) (hs' : optParam (Finset.Nonempty s) (_ : Finset.Nonempty s)) :
Finset.inf' (Finset.map f s) hs g = Finset.inf' s hs' (g f)
theorem Finset.sup'_eq_sup {α : Type u_2} {β : Type u_1} [inst : SemilatticeSup α] [inst : OrderBot α] {s : Finset β} (H : Finset.Nonempty s) (f : βα) :
theorem Finset.sup_closed_of_sup_closed {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderBot α] {s : Set α} (t : Finset α) (htne : Finset.Nonempty t) (h_subset : t s) (h : ∀ (a : α), a s∀ (b : α), b sa b s) :
theorem Finset.coe_sup_of_nonempty {α : Type u_2} {β : Type u_1} [inst : SemilatticeSup α] [inst : OrderBot α] {s : Finset β} (h : Finset.Nonempty s) (f : βα) :
↑(Finset.sup s f) = Finset.sup s (WithBot.some f)
theorem Finset.inf'_eq_inf {α : Type u_2} {β : Type u_1} [inst : SemilatticeInf α] [inst : OrderTop α] {s : Finset β} (H : Finset.Nonempty s) (f : βα) :
theorem Finset.inf_closed_of_inf_closed {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderTop α] {s : Set α} (t : Finset α) (htne : Finset.Nonempty t) (h_subset : t s) (h : ∀ (a : α), a s∀ (b : α), b sa b s) :
theorem Finset.coe_inf_of_nonempty {α : Type u_2} {β : Type u_1} [inst : SemilatticeInf α] [inst : OrderTop α] {s : Finset β} (h : Finset.Nonempty s) (f : βα) :
↑(Finset.inf s f) = Finset.inf s (WithTop.some f)
@[simp]
theorem Finset.sup_apply {α : Type u_2} {β : Type u_3} {C : βType u_1} [inst : (b : β) → SemilatticeSup (C b)] [inst : (b : β) → OrderBot (C b)] (s : Finset α) (f : α(b : β) → C b) (b : β) :
Finset.sup ((b : β) → C b) α Pi.semilatticeSup Pi.orderBot s f b = Finset.sup s fun a => f a b
@[simp]
theorem Finset.inf_apply {α : Type u_2} {β : Type u_3} {C : βType u_1} [inst : (b : β) → SemilatticeInf (C b)] [inst : (b : β) → OrderTop (C b)] (s : Finset α) (f : α(b : β) → C b) (b : β) :
Finset.inf ((b : β) → C b) α Pi.semilatticeInf Pi.orderTop s f b = Finset.inf s fun a => f a b
@[simp]
theorem Finset.sup'_apply {α : Type u_2} {β : Type u_3} {C : βType u_1} [inst : (b : β) → SemilatticeSup (C b)] {s : Finset α} (H : Finset.Nonempty s) (f : α(b : β) → C b) (b : β) :
Finset.sup' ((b : β) → C b) α Pi.semilatticeSup s H f b = Finset.sup' s H fun a => f a b
@[simp]
theorem Finset.inf'_apply {α : Type u_2} {β : Type u_3} {C : βType u_1} [inst : (b : β) → SemilatticeInf (C b)] {s : Finset α} (H : Finset.Nonempty s) (f : α(b : β) → C b) (b : β) :
Finset.inf' ((b : β) → C b) α Pi.semilatticeInf s H f b = Finset.inf' s H fun a => f a b
@[simp]
theorem Finset.toDual_sup' {α : Type u_1} {ι : Type u_2} [inst : SemilatticeSup α] {s : Finset ι} (hs : Finset.Nonempty s) (f : ια) :
OrderDual.toDual (Finset.sup' s hs f) = Finset.inf' s hs (OrderDual.toDual f)
@[simp]
theorem Finset.toDual_inf' {α : Type u_1} {ι : Type u_2} [inst : SemilatticeInf α] {s : Finset ι} (hs : Finset.Nonempty s) (f : ια) :
OrderDual.toDual (Finset.inf' s hs f) = Finset.sup' s hs (OrderDual.toDual f)
@[simp]
theorem Finset.ofDual_sup' {α : Type u_1} {ι : Type u_2} [inst : SemilatticeInf α] {s : Finset ι} (hs : Finset.Nonempty s) (f : ιαᵒᵈ) :
OrderDual.ofDual (Finset.sup' s hs f) = Finset.inf' s hs (OrderDual.ofDual f)
@[simp]
theorem Finset.ofDual_inf' {α : Type u_1} {ι : Type u_2} [inst : SemilatticeSup α] {s : Finset ι} (hs : Finset.Nonempty s) (f : ιαᵒᵈ) :
OrderDual.ofDual (Finset.inf' s hs f) = Finset.sup' s hs (OrderDual.ofDual f)
@[simp]
theorem Finset.le_sup'_iff {α : Type u_1} {ι : Type u_2} [inst : LinearOrder α] {s : Finset ι} (H : Finset.Nonempty s) {f : ια} {a : α} :
a Finset.sup' s H f b, b s a f b
@[simp]
theorem Finset.lt_sup'_iff {α : Type u_1} {ι : Type u_2} [inst : LinearOrder α] {s : Finset ι} (H : Finset.Nonempty s) {f : ια} {a : α} :
a < Finset.sup' s H f b, b s a < f b
@[simp]
theorem Finset.sup'_lt_iff {α : Type u_1} {ι : Type u_2} [inst : LinearOrder α] {s : Finset ι} (H : Finset.Nonempty s) {f : ια} {a : α} :
Finset.sup' s H f < a ∀ (i : ι), i sf i < a
@[simp]
theorem Finset.inf'_le_iff {α : Type u_1} {ι : Type u_2} [inst : LinearOrder α] {s : Finset ι} (H : Finset.Nonempty s) {f : ια} {a : α} :
Finset.inf' s H f a i, i s f i a
@[simp]
theorem Finset.inf'_lt_iff {α : Type u_1} {ι : Type u_2} [inst : LinearOrder α] {s : Finset ι} (H : Finset.Nonempty s) {f : ια} {a : α} :
Finset.inf' s H f < a i, i s f i < a
@[simp]
theorem Finset.lt_inf'_iff {α : Type u_1} {ι : Type u_2} [inst : LinearOrder α] {s : Finset ι} (H : Finset.Nonempty s) {f : ια} {a : α} :
a < Finset.inf' s H f ∀ (i : ι), i sa < f i
theorem Finset.exists_mem_eq_sup' {α : Type u_2} {ι : Type u_1} [inst : LinearOrder α] {s : Finset ι} (H : Finset.Nonempty s) (f : ια) :
i, i s Finset.sup' s H f = f i
theorem Finset.exists_mem_eq_inf' {α : Type u_2} {ι : Type u_1} [inst : LinearOrder α] {s : Finset ι} (H : Finset.Nonempty s) (f : ια) :
i, i s Finset.inf' s H f = f i
theorem Finset.exists_mem_eq_sup {α : Type u_1} {ι : Type u_2} [inst : LinearOrder α] [inst : OrderBot α] (s : Finset ι) (h : Finset.Nonempty s) (f : ια) :
i, i s Finset.sup s f = f i
theorem Finset.exists_mem_eq_inf {α : Type u_1} {ι : Type u_2} [inst : LinearOrder α] [inst : OrderTop α] (s : Finset ι) (h : Finset.Nonempty s) (f : ια) :
i, i s Finset.inf s f = f i

max and min of finite sets #

def Finset.max {α : Type u_1} [inst : LinearOrder α] (s : Finset α) :

Let s be a finset in a linear order. Then s.max is the maximum of s if s is not empty, and ⊥⊥ otherwise. It belongs to WithBot α. If you want to get an element of α, see s.max'.

Equations
theorem Finset.max_eq_sup_coe {α : Type u_1} [inst : LinearOrder α] {s : Finset α} :
Finset.max s = Finset.sup s WithBot.some
theorem Finset.max_eq_sup_withBot {α : Type u_1} [inst : LinearOrder α] (s : Finset α) :
Finset.max s = Finset.sup s WithBot.some
@[simp]
theorem Finset.max_empty {α : Type u_1} [inst : LinearOrder α] :
@[simp]
theorem Finset.max_insert {α : Type u_1} [inst : LinearOrder α] {a : α} {s : Finset α} :
Finset.max (insert a s) = max (a) (Finset.max s)
@[simp]
theorem Finset.max_singleton {α : Type u_1} [inst : LinearOrder α] {a : α} :
Finset.max {a} = a
theorem Finset.max_of_mem {α : Type u_1} [inst : LinearOrder α] {s : Finset α} {a : α} (h : a s) :
b, Finset.max s = b
theorem Finset.max_of_nonempty {α : Type u_1} [inst : LinearOrder α] {s : Finset α} (h : Finset.Nonempty s) :
a, Finset.max s = a
theorem Finset.max_eq_bot {α : Type u_1} [inst : LinearOrder α] {s : Finset α} :
theorem Finset.mem_of_max {α : Type u_1} [inst : LinearOrder α] {s : Finset α} {a : α} :
Finset.max s = aa s
theorem Finset.le_max {α : Type u_1} [inst : LinearOrder α] {a : α} {s : Finset α} (as : a s) :
theorem Finset.not_mem_of_max_lt_coe {α : Type u_1} [inst : LinearOrder α] {a : α} {s : Finset α} (h : Finset.max s < a) :
¬a s
theorem Finset.le_max_of_eq {α : Type u_1} [inst : LinearOrder α] {s : Finset α} {a : α} {b : α} (h₁ : a s) (h₂ : Finset.max s = b) :
a b
theorem Finset.not_mem_of_max_lt {α : Type u_1} [inst : LinearOrder α] {s : Finset α} {a : α} {b : α} (h₁ : b < a) (h₂ : Finset.max s = b) :
¬a s
theorem Finset.max_mono {α : Type u_1} [inst : LinearOrder α] {s : Finset α} {t : Finset α} (st : s t) :
theorem Finset.max_le {α : Type u_1} [inst : LinearOrder α] {M : WithBot α} {s : Finset α} (st : ∀ (a : α), a sa M) :
def Finset.min {α : Type u_1} [inst : LinearOrder α] (s : Finset α) :

Let s be a finset in a linear order. Then s.min is the minimum of s if s is not empty, and ⊤⊤ otherwise. It belongs to WithTop α. If you want to get an element of α, see s.min'.

Equations
theorem Finset.min_eq_inf_withTop {α : Type u_1} [inst : LinearOrder α] (s : Finset α) :
Finset.min s = Finset.inf s WithTop.some
@[simp]
theorem Finset.min_empty {α : Type u_1} [inst : LinearOrder α] :
@[simp]
theorem Finset.min_insert {α : Type u_1} [inst : LinearOrder α] {a : α} {s : Finset α} :
Finset.min (insert a s) = min (a) (Finset.min s)
@[simp]
theorem Finset.min_singleton {α : Type u_1} [inst : LinearOrder α] {a : α} :
Finset.min {a} = a
theorem Finset.min_of_mem {α : Type u_1} [inst : LinearOrder α] {s : Finset α} {a : α} (h : a s) :
b, Finset.min s = b
theorem Finset.min_of_nonempty {α : Type u_1} [inst : LinearOrder α] {s : Finset α} (h : Finset.Nonempty s) :
a, Finset.min s = a
theorem Finset.min_eq_top {α : Type u_1} [inst : LinearOrder α] {s : Finset α} :
theorem Finset.mem_of_min {α : Type u_1} [inst : LinearOrder α] {s : Finset α} {a : α} :
Finset.min s = aa s
theorem Finset.min_le {α : Type u_1} [inst : LinearOrder α] {a : α} {s : Finset α} (as : a s) :
theorem Finset.not_mem_of_coe_lt_min {α : Type u_1} [inst : LinearOrder α] {a : α} {s : Finset α} (h : a < Finset.min s) :
¬a s
theorem Finset.min_le_of_eq {α : Type u_1} [inst : LinearOrder α] {s : Finset α} {a : α} {b : α} (h₁ : b s) (h₂ : Finset.min s = a) :
a b
theorem Finset.not_mem_of_lt_min {α : Type u_1} [inst : LinearOrder α] {s : Finset α} {a : α} {b : α} (h₁ : a < b) (h₂ : Finset.min s = b) :
¬a s
theorem Finset.min_mono {α : Type u_1} [inst : LinearOrder α] {s : Finset α} {t : Finset α} (st : s t) :
theorem Finset.le_min {α : Type u_1} [inst : LinearOrder α] {m : WithTop α} {s : Finset α} (st : ∀ (a : α), a sm a) :
def Finset.min' {α : Type u_1} [inst : LinearOrder α] (s : Finset α) (H : Finset.Nonempty s) :
α

Given a nonempty finset s in a linear order α, then s.min' h is its minimum, as an element of α, where h is a proof of nonemptiness. Without this assumption, use instead s.min, taking values in WithTop α.

Equations
def Finset.max' {α : Type u_1} [inst : LinearOrder α] (s : Finset α) (H : Finset.Nonempty s) :
α

Given a nonempty finset s in a linear order α, then s.max' h is its maximum, as an element of α, where h is a proof of nonemptiness. Without this assumption, use instead s.max, taking values in WithBot α.

Equations
theorem Finset.min'_mem {α : Type u_1} [inst : LinearOrder α] (s : Finset α) (H : Finset.Nonempty s) :
theorem Finset.min'_le {α : Type u_1} [inst : LinearOrder α] (s : Finset α) (x : α) (H2 : x s) :
Finset.min' s (_ : x, x s) x
theorem Finset.le_min' {α : Type u_1} [inst : LinearOrder α] (s : Finset α) (H : Finset.Nonempty s) (x : α) (H2 : ∀ (y : α), y sx y) :
theorem Finset.isLeast_min' {α : Type u_1} [inst : LinearOrder α] (s : Finset α) (H : Finset.Nonempty s) :
IsLeast (s) (Finset.min' s H)
@[simp]
theorem Finset.le_min'_iff {α : Type u_1} [inst : LinearOrder α] (s : Finset α) (H : Finset.Nonempty s) {x : α} :
x Finset.min' s H ∀ (y : α), y sx y
@[simp]
theorem Finset.min'_singleton {α : Type u_1} [inst : LinearOrder α] (a : α) :
Finset.min' {a} (_ : Finset.Nonempty {a}) = a

{a}.min' _ is a.

theorem Finset.max'_mem {α : Type u_1} [inst : LinearOrder α] (s : Finset α) (H : Finset.Nonempty s) :
theorem Finset.le_max' {α : Type u_1} [inst : LinearOrder α] (s : Finset α) (x : α) (H2 : x s) :
x Finset.max' s (_ : x, x s)
theorem Finset.max'_le {α : Type u_1} [inst : LinearOrder α] (s : Finset α) (H : Finset.Nonempty s) (x : α) (H2 : ∀ (y : α), y sy x) :
theorem Finset.isGreatest_max' {α : Type u_1} [inst : LinearOrder α] (s : Finset α) (H : Finset.Nonempty s) :
IsGreatest (s) (Finset.max' s H)
@[simp]
theorem Finset.max'_le_iff {α : Type u_1} [inst : LinearOrder α] (s : Finset α) (H : Finset.Nonempty s) {x : α} :
Finset.max' s H x ∀ (y : α), y sy x
@[simp]
theorem Finset.max'_lt_iff {α : Type u_1} [inst : LinearOrder α] (s : Finset α) (H : Finset.Nonempty s) {x : α} :
Finset.max' s H < x ∀ (y : α), y sy < x
@[simp]
theorem Finset.lt_min'_iff {α : Type u_1} [inst : LinearOrder α] (s : Finset α) (H : Finset.Nonempty s) {x : α} :
x < Finset.min' s H ∀ (y : α), y sx < y
theorem Finset.max'_eq_sup' {α : Type u_1} [inst : LinearOrder α] (s : Finset α) (H : Finset.Nonempty s) :
theorem Finset.min'_eq_inf' {α : Type u_1} [inst : LinearOrder α] (s : Finset α) (H : Finset.Nonempty s) :
@[simp]
theorem Finset.max'_singleton {α : Type u_1} [inst : LinearOrder α] (a : α) :
Finset.max' {a} (_ : Finset.Nonempty {a}) = a

{a}.max' _ is a.

theorem Finset.min'_lt_max' {α : Type u_1} [inst : LinearOrder α] (s : Finset α) {i : α} {j : α} (H1 : i s) (H2 : j s) (H3 : i j) :
Finset.min' s (_ : x, x s) < Finset.max' s (_ : x, x s)
theorem Finset.min'_lt_max'_of_card {α : Type u_1} [inst : LinearOrder α] (s : Finset α) (h₂ : 1 < Finset.card s) :

If there's more than 1 element, the min' is less than the max'. An alternate version of min'_lt_max' which is sometimes more convenient.

theorem Finset.map_ofDual_min {α : Type u_1} [inst : LinearOrder α] (s : Finset αᵒᵈ) :
WithTop.map (OrderDual.ofDual) (Finset.min s) = Finset.max (Finset.image (OrderDual.ofDual) s)
theorem Finset.map_ofDual_max {α : Type u_1} [inst : LinearOrder α] (s : Finset αᵒᵈ) :
WithBot.map (OrderDual.ofDual) (Finset.max s) = Finset.min (Finset.image (OrderDual.ofDual) s)
theorem Finset.map_toDual_min {α : Type u_1} [inst : LinearOrder α] (s : Finset α) :
WithTop.map (OrderDual.toDual) (Finset.min s) = Finset.max (Finset.image (OrderDual.toDual) s)
theorem Finset.map_toDual_max {α : Type u_1} [inst : LinearOrder α] (s : Finset α) :
WithBot.map (OrderDual.toDual) (Finset.max s) = Finset.min (Finset.image (OrderDual.toDual) s)
theorem Finset.ofDual_min' {α : Type u_1} [inst : LinearOrder α] {s : Finset αᵒᵈ} (hs : Finset.Nonempty s) :
OrderDual.ofDual (Finset.min' s hs) = Finset.max' (Finset.image (OrderDual.ofDual) s) (_ : Finset.Nonempty (Finset.image (OrderDual.ofDual) s))
theorem Finset.ofDual_max' {α : Type u_1} [inst : LinearOrder α] {s : Finset αᵒᵈ} (hs : Finset.Nonempty s) :
OrderDual.ofDual (Finset.max' s hs) = Finset.min' (Finset.image (OrderDual.ofDual) s) (_ : Finset.Nonempty (Finset.image (OrderDual.ofDual) s))
theorem Finset.toDual_min' {α : Type u_1} [inst : LinearOrder α] {s : Finset α} (hs : Finset.Nonempty s) :
OrderDual.toDual (Finset.min' s hs) = Finset.max' (Finset.image (OrderDual.toDual) s) (_ : Finset.Nonempty (Finset.image (OrderDual.toDual) s))
theorem Finset.toDual_max' {α : Type u_1} [inst : LinearOrder α] {s : Finset α} (hs : Finset.Nonempty s) :
OrderDual.toDual (Finset.max' s hs) = Finset.min' (Finset.image (OrderDual.toDual) s) (_ : Finset.Nonempty (Finset.image (OrderDual.toDual) s))
theorem Finset.max'_subset {α : Type u_1} [inst : LinearOrder α] {s : Finset α} {t : Finset α} (H : Finset.Nonempty s) (hst : s t) :
theorem Finset.min'_subset {α : Type u_1} [inst : LinearOrder α] {s : Finset α} {t : Finset α} (H : Finset.Nonempty s) (hst : s t) :
theorem Finset.max'_insert {α : Type u_1} [inst : LinearOrder α] (a : α) (s : Finset α) (H : Finset.Nonempty s) :
theorem Finset.min'_insert {α : Type u_1} [inst : LinearOrder α] (a : α) (s : Finset α) (H : Finset.Nonempty s) :
theorem Finset.lt_max'_of_mem_erase_max' {α : Type u_1} [inst : LinearOrder α] (s : Finset α) (H : Finset.Nonempty s) [inst : DecidableEq α] {a : α} (ha : a Finset.erase s (Finset.max' s H)) :
theorem Finset.min'_lt_of_mem_erase_min' {α : Type u_1} [inst : LinearOrder α] (s : Finset α) (H : Finset.Nonempty s) [inst : DecidableEq α] {a : α} (ha : a Finset.erase s (Finset.min' s H)) :
@[simp]
theorem Finset.max'_image {α : Type u_2} {β : Type u_1} [inst : LinearOrder α] [inst : LinearOrder β] {f : αβ} (hf : Monotone f) (s : Finset α) (h : Finset.Nonempty (Finset.image f s)) :
@[simp]
theorem Finset.min'_image {α : Type u_2} {β : Type u_1} [inst : LinearOrder α] [inst : LinearOrder β] {f : αβ} (hf : Monotone f) (s : Finset α) (h : Finset.Nonempty (Finset.image f s)) :
theorem Finset.coe_max' {α : Type u_1} [inst : LinearOrder α] {s : Finset α} (hs : Finset.Nonempty s) :
theorem Finset.coe_min' {α : Type u_1} [inst : LinearOrder α] {s : Finset α} (hs : Finset.Nonempty s) :
theorem Finset.max_mem_image_coe {α : Type u_1} [inst : LinearOrder α] {s : Finset α} (hs : Finset.Nonempty s) :
Finset.max s Finset.image WithBot.some s
theorem Finset.min_mem_image_coe {α : Type u_1} [inst : LinearOrder α] {s : Finset α} (hs : Finset.Nonempty s) :
Finset.min s Finset.image WithTop.some s
theorem Finset.max_mem_insert_bot_image_coe {α : Type u_1} [inst : LinearOrder α] (s : Finset α) :
Finset.max s insert (Finset.image WithBot.some s)
theorem Finset.min_mem_insert_top_image_coe {α : Type u_1} [inst : LinearOrder α] (s : Finset α) :
Finset.min s insert (Finset.image WithTop.some s)
theorem Finset.max'_erase_ne_self {α : Type u_1} [inst : LinearOrder α] {x : α} {s : Finset α} (s0 : Finset.Nonempty (Finset.erase s x)) :
theorem Finset.min'_erase_ne_self {α : Type u_1} [inst : LinearOrder α] {x : α} {s : Finset α} (s0 : Finset.Nonempty (Finset.erase s x)) :
theorem Finset.max_erase_ne_self {α : Type u_1} [inst : LinearOrder α] {x : α} {s : Finset α} :
theorem Finset.min_erase_ne_self {α : Type u_1} [inst : LinearOrder α] {x : α} {s : Finset α} :
theorem Finset.exists_next_right {α : Type u_1} [inst : LinearOrder α] {x : α} {s : Finset α} (h : y, y s x < y) :
y, y s x < y ∀ (z : α), z sx < zy z
theorem Finset.exists_next_left {α : Type u_1} [inst : LinearOrder α] {x : α} {s : Finset α} (h : y, y s y < x) :
y, y s y < x ∀ (z : α), z sz < xz y
theorem Finset.card_le_of_interleaved {α : Type u_1} [inst : LinearOrder α] {s : Finset α} {t : Finset α} (h : ∀ (x : α), x s∀ (y : α), y sx < y(∀ (z : α), z s¬z Set.Ioo x y) → z, z t x < z z < y) :

If finsets s and t are interleaved, then Finset.card s ≤ Finset.card t + 1≤ Finset.card t + 1.

theorem Finset.card_le_diff_of_interleaved {α : Type u_1} [inst : LinearOrder α] {s : Finset α} {t : Finset α} (h : ∀ (x : α), x s∀ (y : α), y sx < y(∀ (z : α), z s¬z Set.Ioo x y) → z, z t x < z z < y) :

If finsets s and t are interleaved, then Finset.card s ≤ Finset.card (t \ s) + 1≤ Finset.card (t \ s) + 1.

theorem Finset.induction_on_max {α : Type u_1} [inst : LinearOrder α] [inst : DecidableEq α] {p : Finset αProp} (s : Finset α) (h0 : p ) (step : (a : α) → (s : Finset α) → (∀ (x : α), x sx < a) → p sp (insert a s)) :
p s

Induction principle for Finsets in a linearly ordered type: a predicate is true on all s : Finset α provided that:

  • it is true on the empty Finset,
  • for every s : Finset α and an element a strictly greater than all elements of s, p s implies p (insert a s).
theorem Finset.induction_on_min {α : Type u_1} [inst : LinearOrder α] [inst : DecidableEq α] {p : Finset αProp} (s : Finset α) (h0 : p ) (step : (a : α) → (s : Finset α) → (∀ (x : α), x sa < x) → p sp (insert a s)) :
p s

Induction principle for Finsets in a linearly ordered type: a predicate is true on all s : Finset α provided that:

  • it is true on the empty Finset,
  • for every s : Finset α and an element a strictly less than all elements of s, p s implies p (insert a s).
theorem Finset.induction_on_max_value {α : Type u_2} {ι : Type u_1} [inst : LinearOrder α] [inst : DecidableEq ι] (f : ια) {p : Finset ιProp} (s : Finset ι) (h0 : p ) (step : (a : ι) → (s : Finset ι) → ¬a s(∀ (x : ι), x sf x f a) → p sp (insert a s)) :
p s

Induction principle for Finsets in any type from which a given function f maps to a linearly ordered type : a predicate is true on all s : Finset α provided that:

  • it is true on the empty Finset,
  • for every s : Finset α and an element a such that for elements of s denoted by x we have f x ≤ f a≤ f a, p s implies p (insert a s).
theorem Finset.induction_on_min_value {α : Type u_2} {ι : Type u_1} [inst : LinearOrder α] [inst : DecidableEq ι] (f : ια) {p : Finset ιProp} (s : Finset ι) (h0 : p ) (step : (a : ι) → (s : Finset ι) → ¬a s(∀ (x : ι), x sf a f x) → p sp (insert a s)) :
p s

Induction principle for Finsets in any type from which a given function f maps to a linearly ordered type : a predicate is true on all s : Finset α provided that:

  • it is true on the empty Finset,
  • for every s : Finset α and an element a such that for elements of s denoted by x we have f a ≤ f x≤ f x, p s implies p (insert a s).
theorem Finset.exists_max_image {α : Type u_2} {β : Type u_1} [inst : LinearOrder α] (s : Finset β) (f : βα) (h : Finset.Nonempty s) :
x, x s ∀ (x' : β), x' sf x' f x
theorem Finset.exists_min_image {α : Type u_2} {β : Type u_1} [inst : LinearOrder α] (s : Finset β) (f : βα) (h : Finset.Nonempty s) :
x, x s ∀ (x' : β), x' sf x f x'
theorem Finset.is_glb_iff_is_least {α : Type u_1} [inst : LinearOrder α] (i : α) (s : Finset α) (hs : Finset.Nonempty s) :
IsGLB (s) i IsLeast (s) i
theorem Finset.is_lub_iff_is_greatest {α : Type u_1} [inst : LinearOrder α] (i : α) (s : Finset α) (hs : Finset.Nonempty s) :
IsLUB (s) i IsGreatest (s) i
theorem Finset.is_glb_mem {α : Type u_1} [inst : LinearOrder α] {i : α} (s : Finset α) (his : IsGLB (s) i) (hs : Finset.Nonempty s) :
i s
theorem Finset.is_lub_mem {α : Type u_1} [inst : LinearOrder α] {i : α} (s : Finset α) (his : IsLUB (s) i) (hs : Finset.Nonempty s) :
i s
theorem Multiset.map_finset_sup {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : DecidableEq α] [inst : DecidableEq β] (s : Finset γ) (f : γMultiset β) (g : βα) (hg : Function.Injective g) :
theorem Multiset.count_finset_sup {α : Type u_2} {β : Type u_1} [inst : DecidableEq β] (s : Finset α) (f : αMultiset β) (b : β) :
theorem Multiset.mem_sup {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {s : Finset α} {f : αMultiset β} {x : β} :
x Finset.sup s f v, v s x f v
theorem Finset.mem_sup {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {s : Finset α} {f : αFinset β} {x : β} :
x Finset.sup s f v, v s x f v
theorem Finset.sup_eq_bunionᵢ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (s : Finset α) (t : αFinset β) :
@[simp]
theorem Finset.sup_singleton'' {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] (s : Finset β) (f : βα) :
(Finset.sup s fun b => {f b}) = Finset.image f s
@[simp]
theorem Finset.sup_singleton' {α : Type u_1} [inst : DecidableEq α] (s : Finset α) :
Finset.sup s singleton = s
theorem supᵢ_eq_supᵢ_finset {α : Type u_1} {ι : Type u_2} [inst : CompleteLattice α] (s : ια) :
(i, s i) = t, i, h, s i

Supremum of s i, i : ι, is equal to the supremum over t : Finset ι of suprema ⨆ i ∈ t, s i⨆ i ∈ t, s i∈ t, s i. This version assumes ι is a Type _. See supᵢ_eq_supᵢ_finset' for a version that works for ι : Sort*.

theorem supᵢ_eq_supᵢ_finset' {α : Type u_1} {ι' : Sort u_2} [inst : CompleteLattice α] (s : ι'α) :
(i, s i) = t, i, h, s i.down

Supremum of s i, i : ι, is equal to the supremum over t : Finset ι of suprema ⨆ i ∈ t, s i⨆ i ∈ t, s i∈ t, s i. This version works for ι : Sort*. See supᵢ_eq_supᵢ_finset for a version that assumes ι : Type _ but has no plifts.

theorem infᵢ_eq_infᵢ_finset {α : Type u_1} {ι : Type u_2} [inst : CompleteLattice α] (s : ια) :
(i, s i) = t, i, h, s i

Infimum of s i, i : ι, is equal to the infimum over t : Finset ι of infima ⨅ i ∈ t, s i⨅ i ∈ t, s i∈ t, s i. This version assumes ι is a Type _. See infᵢ_eq_infᵢ_finset' for a version that works for ι : Sort*.

theorem infᵢ_eq_infᵢ_finset' {α : Type u_1} {ι' : Sort u_2} [inst : CompleteLattice α] (s : ι'α) :
(i, s i) = t, i, h, s i.down

Infimum of s i, i : ι, is equal to the infimum over t : Finset ι of infima ⨅ i ∈ t, s i⨅ i ∈ t, s i∈ t, s i. This version works for ι : Sort*. See infᵢ_eq_infᵢ_finset for a version that assumes ι : Type _ but has no plifts.

theorem Set.unionᵢ_eq_unionᵢ_finset {α : Type u_1} {ι : Type u_2} (s : ιSet α) :
(Set.unionᵢ fun i => s i) = Set.unionᵢ fun t => Set.unionᵢ fun i => Set.unionᵢ fun h => s i

Union of an indexed family of sets s : ι → Set α→ Set α is equal to the union of the unions of finite subfamilies. This version assumes ι : Type _. See also unionᵢ_eq_unionᵢ_finset' for a version that works for ι : Sort*.

theorem Set.unionᵢ_eq_unionᵢ_finset' {α : Type u_1} {ι' : Sort u_2} (s : ι'Set α) :
(Set.unionᵢ fun i => s i) = Set.unionᵢ fun t => Set.unionᵢ fun i => Set.unionᵢ fun h => s i.down

Union of an indexed family of sets s : ι → Set α→ Set α is equal to the union of the unions of finite subfamilies. This version works for ι : Sort*. See also unionᵢ_eq_unionᵢ_finset for a version that assumes ι : Type _ but avoids plifts in the right hand side.

theorem Set.interᵢ_eq_interᵢ_finset {α : Type u_1} {ι : Type u_2} (s : ιSet α) :
(Set.interᵢ fun i => s i) = Set.interᵢ fun t => Set.interᵢ fun i => Set.interᵢ fun h => s i

Intersection of an indexed family of sets s : ι → Set α→ Set α is equal to the intersection of the intersections of finite subfamilies. This version assumes ι : Type _. See also interᵢ_eq_interᵢ_finset' for a version that works for ι : Sort*.

theorem Set.interᵢ_eq_interᵢ_finset' {α : Type u_1} {ι' : Sort u_2} (s : ι'Set α) :
(Set.interᵢ fun i => s i) = Set.interᵢ fun t => Set.interᵢ fun i => Set.interᵢ fun h => s i.down

Intersection of an indexed family of sets s : ι → Set α→ Set α is equal to the intersection of the intersections of finite subfamilies. This version works for ι : Sort*. See also interᵢ_eq_interᵢ_finset for a version that assumes ι : Type _ but avoids plifts in the right hand side.

Interaction with ordered algebra structures #

theorem Finset.sup_mul_le_mul_sup_of_nonneg {α : Type u_1} {ι : Type u_2} [inst : LinearOrderedSemiring α] [inst : OrderBot α] {a : ια} {b : ια} (s : Finset ι) (ha : ∀ (i : ι), i s0 a i) (hb : ∀ (i : ι), i s0 b i) :
theorem Finset.mul_inf_le_inf_mul_of_nonneg {α : Type u_1} {ι : Type u_2} [inst : LinearOrderedSemiring α] [inst : OrderTop α] {a : ια} {b : ια} (s : Finset ι) (ha : ∀ (i : ι), i s0 a i) (hb : ∀ (i : ι), i s0 b i) :
theorem Finset.sup'_mul_le_mul_sup'_of_nonneg {α : Type u_1} {ι : Type u_2} [inst : LinearOrderedSemiring α] {a : ια} {b : ια} (s : Finset ι) (H : Finset.Nonempty s) (ha : ∀ (i : ι), i s0 a i) (hb : ∀ (i : ι), i s0 b i) :
Finset.sup' s H (a * b) Finset.sup' s H a * Finset.sup' s H b
theorem Finset.inf'_mul_le_mul_inf'_of_nonneg {α : Type u_1} {ι : Type u_2} [inst : LinearOrderedSemiring α] {a : ια} {b : ια} (s : Finset ι) (H : Finset.Nonempty s) (ha : ∀ (i : ι), i s0 a i) (hb : ∀ (i : ι), i s0 b i) :
Finset.inf' s H a * Finset.inf' s H b Finset.inf' s H (a * b)

Interaction with big lattice/set operations #

theorem Finset.supᵢ_coe {α : Type u_2} {β : Type u_1} [inst : SupSet β] (f : αβ) (s : Finset α) :
(x, h, f x) = x, h, f x
theorem Finset.infᵢ_coe {α : Type u_2} {β : Type u_1} [inst : InfSet β] (f : αβ) (s : Finset α) :
(x, h, f x) = x, h, f x
theorem Finset.supᵢ_singleton {α : Type u_2} {β : Type u_1} [inst : CompleteLattice β] (a : α) (s : αβ) :
(x, h, s x) = s a
theorem Finset.infᵢ_singleton {α : Type u_2} {β : Type u_1} [inst : CompleteLattice β] (a : α) (s : αβ) :
(x, h, s x) = s a
theorem Finset.supᵢ_option_toFinset {α : Type u_1} {β : Type u_2} [inst : CompleteLattice β] (o : Option α) (f : αβ) :
(x, h, f x) = x, h, f x
theorem Finset.infᵢ_option_toFinset {α : Type u_1} {β : Type u_2} [inst : CompleteLattice β] (o : Option α) (f : αβ) :
(x, h, f x) = x, h, f x
theorem Finset.supᵢ_union {α : Type u_1} {β : Type u_2} [inst : CompleteLattice β] [inst : DecidableEq α] {f : αβ} {s : Finset α} {t : Finset α} :
(x, h, f x) = (x, h, f x) x, h, f x
theorem Finset.infᵢ_union {α : Type u_1} {β : Type u_2} [inst : CompleteLattice β] [inst : DecidableEq α] {f : αβ} {s : Finset α} {t : Finset α} :
(x, h, f x) = (x, h, f x) x, h, f x
theorem Finset.supᵢ_insert {α : Type u_1} {β : Type u_2} [inst : CompleteLattice β] [inst : DecidableEq α] (a : α) (s : Finset α) (t : αβ) :
(x, h, t x) = t a x, h, t x
theorem Finset.infᵢ_insert {α : Type u_1} {β : Type u_2} [inst : CompleteLattice β] [inst : DecidableEq α] (a : α) (s : Finset α) (t : αβ) :
(x, h, t x) = t a x, h, t x
theorem Finset.supᵢ_finset_image {α : Type u_3} {β : Type u_2} {γ : Type u_1} [inst : CompleteLattice β] [inst : DecidableEq α] {f : γα} {g : αβ} {s : Finset γ} :
(x, h, g x) = y, h, g (f y)
theorem Finset.sup_finset_image {α : Type u_3} [inst : DecidableEq α] {β : Type u_1} {γ : Type u_2} [inst : SemilatticeSup β] [inst : OrderBot β] (f : γα) (g : αβ) (s : Finset γ) :
theorem Finset.infᵢ_finset_image {α : Type u_3} {β : Type u_2} {γ : Type u_1} [inst : CompleteLattice β] [inst : DecidableEq α] {f : γα} {g : αβ} {s : Finset γ} :
(x, h, g x) = y, h, g (f y)
theorem Finset.supᵢ_insert_update {α : Type u_1} {β : Type u_2} [inst : CompleteLattice β] [inst : DecidableEq α] {x : α} {t : Finset α} (f : αβ) {s : β} (hx : ¬x t) :
(i, h, Function.update f x s i) = s i, h, f i
theorem Finset.infᵢ_insert_update {α : Type u_1} {β : Type u_2} [inst : CompleteLattice β] [inst : DecidableEq α] {x : α} {t : Finset α} (f : αβ) {s : β} (hx : ¬x t) :
(i, h, Function.update f x s i) = s i, h, f i
theorem Finset.supᵢ_bunionᵢ {α : Type u_2} {β : Type u_3} {γ : Type u_1} [inst : CompleteLattice β] [inst : DecidableEq α] (s : Finset γ) (t : γFinset α) (f : αβ) :
(y, h, f y) = x, h, y, h, f y
theorem Finset.infᵢ_bunionᵢ {α : Type u_2} {β : Type u_3} {γ : Type u_1} [inst : CompleteLattice β] [inst : DecidableEq α] (s : Finset γ) (t : γFinset α) (f : αβ) :
(y, h, f y) = x, h, y, h, f y
theorem Finset.set_bunionᵢ_coe {α : Type u_1} {β : Type u_2} (s : Finset α) (t : αSet β) :
(Set.unionᵢ fun x => Set.unionᵢ fun h => t x) = Set.unionᵢ fun x => Set.unionᵢ fun h => t x
theorem Finset.set_binterᵢ_coe {α : Type u_1} {β : Type u_2} (s : Finset α) (t : αSet β) :
(Set.interᵢ fun x => Set.interᵢ fun h => t x) = Set.interᵢ fun x => Set.interᵢ fun h => t x
theorem Finset.set_bunionᵢ_singleton {α : Type u_2} {β : Type u_1} (a : α) (s : αSet β) :
(Set.unionᵢ fun x => Set.unionᵢ fun h => s x) = s a
theorem Finset.set_binterᵢ_singleton {α : Type u_2} {β : Type u_1} (a : α) (s : αSet β) :
(Set.interᵢ fun x => Set.interᵢ fun h => s x) = s a
@[simp]
theorem Finset.set_bunionᵢ_preimage_singleton {α : Type u_2} {β : Type u_1} (f : αβ) (s : Finset β) :
(Set.unionᵢ fun y => Set.unionᵢ fun h => f ⁻¹' {y}) = f ⁻¹' s
theorem Finset.set_bunionᵢ_option_toFinset {α : Type u_1} {β : Type u_2} (o : Option α) (f : αSet β) :
(Set.unionᵢ fun x => Set.unionᵢ fun h => f x) = Set.unionᵢ fun x => Set.unionᵢ fun h => f x
theorem Finset.set_binterᵢ_option_toFinset {α : Type u_1} {β : Type u_2} (o : Option α) (f : αSet β) :
(Set.interᵢ fun x => Set.interᵢ fun h => f x) = Set.interᵢ fun x => Set.interᵢ fun h => f x
theorem Finset.subset_set_bunionᵢ_of_mem {α : Type u_1} {β : Type u_2} {s : Finset α} {f : αSet β} {x : α} (h : x s) :
f x Set.unionᵢ fun y => Set.unionᵢ fun h => f y
theorem Finset.set_bunionᵢ_union {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] (s : Finset α) (t : Finset α) (u : αSet β) :
(Set.unionᵢ fun x => Set.unionᵢ fun h => u x) = (Set.unionᵢ fun x => Set.unionᵢ fun h => u x) Set.unionᵢ fun x => Set.unionᵢ fun h => u x
theorem Finset.set_binterᵢ_inter {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] (s : Finset α) (t : Finset α) (u : αSet β) :
(Set.interᵢ fun x => Set.interᵢ fun h => u x) = (Set.interᵢ fun x => Set.interᵢ fun h => u x) Set.interᵢ fun x => Set.interᵢ fun h => u x
theorem Finset.set_bunionᵢ_insert {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] (a : α) (s : Finset α) (t : αSet β) :
(Set.unionᵢ fun x => Set.unionᵢ fun h => t x) = t a Set.unionᵢ fun x => Set.unionᵢ fun h => t x
theorem Finset.set_binterᵢ_insert {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] (a : α) (s : Finset α) (t : αSet β) :
(Set.interᵢ fun x => Set.interᵢ fun h => t x) = t a Set.interᵢ fun x => Set.interᵢ fun h => t x
theorem Finset.set_bunionᵢ_finset_image {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : DecidableEq α] {f : γα} {g : αSet β} {s : Finset γ} :
(Set.unionᵢ fun x => Set.unionᵢ fun h => g x) = Set.unionᵢ fun y => Set.unionᵢ fun h => g (f y)
theorem Finset.set_binterᵢ_finset_image {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : DecidableEq α] {f : γα} {g : αSet β} {s : Finset γ} :
(Set.interᵢ fun x => Set.interᵢ fun h => g x) = Set.interᵢ fun y => Set.interᵢ fun h => g (f y)
theorem Finset.set_bunionᵢ_insert_update {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] {x : α} {t : Finset α} (f : αSet β) {s : Set β} (hx : ¬x t) :
(Set.unionᵢ fun i => Set.unionᵢ fun h => Function.update f x s i) = s Set.unionᵢ fun i => Set.unionᵢ fun h => f i
theorem Finset.set_binterᵢ_insert_update {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] {x : α} {t : Finset α} (f : αSet β) {s : Set β} (hx : ¬x t) :
(Set.interᵢ fun i => Set.interᵢ fun h => Function.update f x s i) = s Set.interᵢ fun i => Set.interᵢ fun h => f i
theorem Finset.set_bunionᵢ_bunionᵢ {α : Type u_2} {β : Type u_3} {γ : Type u_1} [inst : DecidableEq α] (s : Finset γ) (t : γFinset α) (f : αSet β) :
(Set.unionᵢ fun y => Set.unionᵢ fun h => f y) = Set.unionᵢ fun x => Set.unionᵢ fun h => Set.unionᵢ fun y => Set.unionᵢ fun h => f y
theorem Finset.set_binterᵢ_bunionᵢ {α : Type u_2} {β : Type u_3} {γ : Type u_1} [inst : DecidableEq α] (s : Finset γ) (t : γFinset α) (f : αSet β) :
(Set.interᵢ fun y => Set.interᵢ fun h => f y) = Set.interᵢ fun x => Set.interᵢ fun h => Set.interᵢ fun y => Set.interᵢ fun h => f y