Lattice operations on finsets #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
sup #
def
finset.sup
{α : Type u_2}
{β : Type u_3}
[semilattice_sup α]
[order_bot α]
(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 has_sup.sup ⊥ f s
Instances for ↥finset.sup
theorem
finset.sup_def
{α : Type u_2}
{β : Type u_3}
[semilattice_sup α]
[order_bot α]
{s : finset β}
{f : β → α} :
s.sup f = (multiset.map f s.val).sup
@[simp]
theorem
finset.sup_cons
{α : Type u_2}
{β : Type u_3}
[semilattice_sup α]
[order_bot α]
{s : finset β}
{f : β → α}
{b : β}
(h : b ∉ s) :
(finset.cons b s h).sup f = f b ⊔ s.sup f
@[simp]
theorem
finset.sup_insert
{α : Type u_2}
{β : Type u_3}
[semilattice_sup α]
[order_bot α]
{s : finset β}
{f : β → α}
[decidable_eq β]
{b : β} :
(has_insert.insert b s).sup f = f b ⊔ s.sup f
theorem
finset.sup_image
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[semilattice_sup α]
[order_bot α]
[decidable_eq β]
(s : finset γ)
(f : γ → β)
(g : β → α) :
(finset.image f s).sup g = s.sup (g ∘ f)
@[simp]
theorem
finset.sup_singleton
{α : Type u_2}
{β : Type u_3}
[semilattice_sup α]
[order_bot α]
{f : β → α}
{b : β} :
@[simp]
theorem
map_finset_sup
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
{ι : Type u_5}
[semilattice_sup α]
[order_bot α]
[semilattice_sup β]
[order_bot β]
[sup_bot_hom_class F α β]
(f : F)
(s : finset ι)
(g : ι → α) :
theorem
finset.sup_const_le
{α : Type u_2}
{β : Type u_3}
[semilattice_sup α]
[order_bot α]
{s : finset β}
{a : α} :
theorem
finset.sup_union
{α : Type u_2}
{β : Type u_3}
[semilattice_sup α]
[order_bot α]
{s₁ s₂ : finset β}
{f : β → α}
[decidable_eq β] :
theorem
finset.sup_const
{α : Type u_2}
{β : Type u_3}
[semilattice_sup α]
[order_bot α]
{s : finset β}
(h : s.nonempty)
(c : α) :
theorem
finset.sup_ite
{α : Type u_2}
{β : Type u_3}
[semilattice_sup α]
[order_bot α]
{s : finset β}
{f g : β → α}
(p : β → Prop)
[decidable_pred p] :
s.sup (λ (i : β), ite (p i) (f i) (g i)) = (finset.filter p s).sup f ⊔ (finset.filter (λ (i : β), ¬p i) s).sup g
@[simp]
theorem
finset.sup_erase_bot
{α : Type u_2}
[semilattice_sup α]
[order_bot α]
[decidable_eq α]
(s : finset α) :
theorem
list.foldr_sup_eq_sup_to_finset
{α : Type u_2}
[semilattice_sup α]
[order_bot α]
[decidable_eq α]
(l : list α) :
list.foldr has_sup.sup ⊥ l = l.to_finset.sup id
theorem
finset.sup_id_eq_Sup
{α : Type u_2}
[complete_lattice α]
(s : finset α) :
s.sup id = has_Sup.Sup ↑s
theorem
finset.sup_eq_Sup_image
{α : Type u_2}
{β : Type u_3}
[complete_lattice β]
(s : finset α)
(f : α → β) :
s.sup f = has_Sup.Sup (f '' ↑s)
inf #
def
finset.inf
{α : Type u_2}
{β : Type u_3}
[semilattice_inf α]
[order_top α]
(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 has_inf.inf ⊤ f s
theorem
finset.inf_def
{α : Type u_2}
{β : Type u_3}
[semilattice_inf α]
[order_top α]
{s : finset β}
{f : β → α} :
s.inf f = (multiset.map f s.val).inf
@[simp]
theorem
finset.inf_cons
{α : Type u_2}
{β : Type u_3}
[semilattice_inf α]
[order_top α]
{s : finset β}
{f : β → α}
{b : β}
(h : b ∉ s) :
(finset.cons b s h).inf f = f b ⊓ s.inf f
@[simp]
theorem
finset.inf_insert
{α : Type u_2}
{β : Type u_3}
[semilattice_inf α]
[order_top α]
{s : finset β}
{f : β → α}
[decidable_eq β]
{b : β} :
(has_insert.insert b s).inf f = f b ⊓ s.inf f
theorem
finset.inf_image
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[semilattice_inf α]
[order_top α]
[decidable_eq β]
(s : finset γ)
(f : γ → β)
(g : β → α) :
(finset.image f s).inf g = s.inf (g ∘ f)
@[simp]
theorem
finset.inf_singleton
{α : Type u_2}
{β : Type u_3}
[semilattice_inf α]
[order_top α]
{f : β → α}
{b : β} :
@[simp]
theorem
map_finset_inf
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
{ι : Type u_5}
[semilattice_inf α]
[order_top α]
[semilattice_inf β]
[order_top β]
[inf_top_hom_class F α β]
(f : F)
(s : finset ι)
(g : ι → α) :
theorem
finset.inf_union
{α : Type u_2}
{β : Type u_3}
[semilattice_inf α]
[order_top α]
{s₁ s₂ : finset β}
{f : β → α}
[decidable_eq β] :
theorem
finset.inf_const
{α : Type u_2}
{β : Type u_3}
[semilattice_inf α]
[order_top α]
{s : finset β}
(h : s.nonempty)
(c : α) :
theorem
finset.le_inf_const_le
{α : Type u_2}
{β : Type u_3}
[semilattice_inf α]
[order_top α]
{s : finset β}
{a : α} :
@[simp]
theorem
finset.inf_erase_top
{α : Type u_2}
[semilattice_inf α]
[order_top α]
[decidable_eq α]
(s : finset α) :
theorem
list.foldr_inf_eq_inf_to_finset
{α : Type u_2}
[semilattice_inf α]
[order_top α]
[decidable_eq α]
(l : list α) :
list.foldr has_inf.inf ⊤ l = l.to_finset.inf id
@[simp]
theorem
finset.to_dual_sup
{α : Type u_2}
{β : Type u_3}
[semilattice_sup α]
[order_bot α]
(s : finset β)
(f : β → α) :
⇑order_dual.to_dual (s.sup f) = s.inf (⇑order_dual.to_dual ∘ f)
@[simp]
theorem
finset.to_dual_inf
{α : Type u_2}
{β : Type u_3}
[semilattice_inf α]
[order_top α]
(s : finset β)
(f : β → α) :
⇑order_dual.to_dual (s.inf f) = s.sup (⇑order_dual.to_dual ∘ f)
@[simp]
theorem
finset.of_dual_sup
{α : Type u_2}
{β : Type u_3}
[semilattice_inf α]
[order_top α]
(s : finset β)
(f : β → αᵒᵈ) :
⇑order_dual.of_dual (s.sup f) = s.inf (⇑order_dual.of_dual ∘ f)
@[simp]
theorem
finset.of_dual_inf
{α : Type u_2}
{β : Type u_3}
[semilattice_sup α]
[order_bot α]
(s : finset β)
(f : β → αᵒᵈ) :
⇑order_dual.of_dual (s.inf f) = s.sup (⇑order_dual.of_dual ∘ f)
@[protected]
theorem
finset.codisjoint_inf_right
{α : Type u_2}
{ι : Type u_5}
[distrib_lattice α]
[order_top α]
{f : ι → α}
{s : finset ι}
{a : α} :
codisjoint a (s.inf f) ↔ ∀ ⦃i : ι⦄, i ∈ s → codisjoint a (f i)
@[protected]
theorem
finset.codisjoint_inf_left
{α : Type u_2}
{ι : Type u_5}
[distrib_lattice α]
[order_top α]
{f : ι → α}
{s : finset ι}
{a : α} :
codisjoint (s.inf f) a ↔ ∀ ⦃i : ι⦄, i ∈ s → codisjoint (f i) a
theorem
finset.inf_sup
{α : Type u_2}
{ι : Type u_5}
[distrib_lattice α]
[bounded_order α]
[decidable_eq ι]
{κ : ι → Type u_1}
(s : finset ι)
(t : Π (i : ι), finset (κ i))
(f : Π (i : ι), κ i → α) :
theorem
finset.sup_inf
{α : Type u_2}
{ι : Type u_5}
[distrib_lattice α]
[bounded_order α]
[decidable_eq ι]
{κ : ι → Type u_1}
(s : finset ι)
(t : Π (i : ι), finset (κ i))
(f : Π (i : ι), κ i → α) :
theorem
finset.inf_id_eq_Inf
{α : Type u_2}
[complete_lattice α]
(s : finset α) :
s.inf id = has_Inf.Inf ↑s
theorem
finset.inf_eq_Inf_image
{α : Type u_2}
{β : Type u_3}
[complete_lattice β]
(s : finset α)
(f : α → β) :
s.inf f = has_Inf.Inf (f '' ↑s)
def
finset.sup'
{α : Type u_2}
{β : Type u_3}
[semilattice_sup α]
(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.
@[simp]
theorem
finset.sup'_cons
{α : Type u_2}
{β : Type u_3}
[semilattice_sup α]
{s : finset β}
(H : s.nonempty)
(f : β → α)
{b : β}
{hb : b ∉ s}
{h : (finset.cons b s hb).nonempty} :
(finset.cons b s hb).sup' h f = f b ⊔ s.sup' H f
@[simp]
theorem
finset.sup'_insert
{α : Type u_2}
{β : Type u_3}
[semilattice_sup α]
{s : finset β}
(H : s.nonempty)
(f : β → α)
[decidable_eq β]
{b : β}
{h : (has_insert.insert b s).nonempty} :
(has_insert.insert b s).sup' h f = f b ⊔ s.sup' H f
@[simp]
theorem
finset.sup'_singleton
{α : Type u_2}
{β : Type u_3}
[semilattice_sup α]
(f : β → α)
{b : β}
{h : {b}.nonempty} :
theorem
finset.le_sup'
{α : Type u_2}
{β : Type u_3}
[semilattice_sup α]
{s : finset β}
(f : β → α)
{b : β}
(h : b ∈ s) :
@[simp]
theorem
finset.sup'_const
{α : Type u_2}
{β : Type u_3}
[semilattice_sup α]
{s : finset β}
(H : s.nonempty)
(a : α) :
@[simp]
theorem
map_finset_sup'
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
{ι : Type u_5}
[semilattice_sup α]
[semilattice_sup β]
[sup_hom_class F α β]
(f : F)
{s : finset ι}
(hs : s.nonempty)
(g : ι → α) :
@[simp]
theorem
finset.sup'_image
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[semilattice_sup α]
[decidable_eq β]
{s : finset γ}
{f : γ → β}
(hs : (finset.image f s).nonempty)
(g : β → α)
(hs' : s.nonempty := _) :
(finset.image f s).sup' hs g = s.sup' hs' (g ∘ f)
@[simp]
theorem
finset.sup'_map
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[semilattice_sup α]
{s : finset γ}
{f : γ ↪ β}
(g : β → α)
(hs : (finset.map f s).nonempty)
(hs' : s.nonempty := _) :
def
finset.inf'
{α : Type u_2}
{β : Type u_3}
[semilattice_inf α]
(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.
@[simp]
theorem
finset.inf'_cons
{α : Type u_2}
{β : Type u_3}
[semilattice_inf α]
{s : finset β}
(H : s.nonempty)
(f : β → α)
{b : β}
{hb : b ∉ s}
{h : (finset.cons b s hb).nonempty} :
(finset.cons b s hb).inf' h f = f b ⊓ s.inf' H f
@[simp]
theorem
finset.inf'_insert
{α : Type u_2}
{β : Type u_3}
[semilattice_inf α]
{s : finset β}
(H : s.nonempty)
(f : β → α)
[decidable_eq β]
{b : β}
{h : (has_insert.insert b s).nonempty} :
(has_insert.insert b s).inf' h f = f b ⊓ s.inf' H f
@[simp]
theorem
finset.inf'_singleton
{α : Type u_2}
{β : Type u_3}
[semilattice_inf α]
(f : β → α)
{b : β}
{h : {b}.nonempty} :
theorem
finset.inf'_le
{α : Type u_2}
{β : Type u_3}
[semilattice_inf α]
{s : finset β}
(f : β → α)
{b : β}
(h : b ∈ s) :
@[simp]
theorem
finset.inf'_const
{α : Type u_2}
{β : Type u_3}
[semilattice_inf α]
{s : finset β}
(H : s.nonempty)
(a : α) :
@[simp]
theorem
map_finset_inf'
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
{ι : Type u_5}
[semilattice_inf α]
[semilattice_inf β]
[inf_hom_class F α β]
(f : F)
{s : finset ι}
(hs : s.nonempty)
(g : ι → α) :
@[simp]
theorem
finset.inf'_image
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[semilattice_inf α]
[decidable_eq β]
{s : finset γ}
{f : γ → β}
(hs : (finset.image f s).nonempty)
(g : β → α)
(hs' : s.nonempty := _) :
(finset.image f s).inf' hs g = s.inf' hs' (g ∘ f)
@[simp]
theorem
finset.inf'_map
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[semilattice_inf α]
{s : finset γ}
{f : γ ↪ β}
(g : β → α)
(hs : (finset.map f s).nonempty)
(hs' : s.nonempty := _) :
@[simp]
theorem
finset.to_dual_sup'
{α : Type u_2}
{ι : Type u_5}
[semilattice_sup α]
{s : finset ι}
(hs : s.nonempty)
(f : ι → α) :
⇑order_dual.to_dual (s.sup' hs f) = s.inf' hs (⇑order_dual.to_dual ∘ f)
@[simp]
theorem
finset.to_dual_inf'
{α : Type u_2}
{ι : Type u_5}
[semilattice_inf α]
{s : finset ι}
(hs : s.nonempty)
(f : ι → α) :
⇑order_dual.to_dual (s.inf' hs f) = s.sup' hs (⇑order_dual.to_dual ∘ f)
@[simp]
theorem
finset.of_dual_sup'
{α : Type u_2}
{ι : Type u_5}
[semilattice_inf α]
{s : finset ι}
(hs : s.nonempty)
(f : ι → αᵒᵈ) :
⇑order_dual.of_dual (s.sup' hs f) = s.inf' hs (⇑order_dual.of_dual ∘ f)
@[simp]
theorem
finset.of_dual_inf'
{α : Type u_2}
{ι : Type u_5}
[semilattice_sup α]
{s : finset ι}
(hs : s.nonempty)
(f : ι → αᵒᵈ) :
⇑order_dual.of_dual (s.inf' hs f) = s.sup' hs (⇑order_dual.of_dual ∘ f)
max and min of finite sets #
@[protected]
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 with_bot α. If you want to get an element of α, see
s.max'.
@[simp]
theorem
finset.max_insert
{α : Type u_2}
[linear_order α]
{a : α}
{s : finset α} :
(has_insert.insert a s).max = linear_order.max ↑a s.max
theorem
finset.not_mem_of_max_lt_coe
{α : Type u_2}
[linear_order α]
{a : α}
{s : finset α}
(h : s.max < ↑a) :
a ∉ s
theorem
finset.le_max_of_eq
{α : Type u_2}
[linear_order α]
{s : finset α}
{a b : α}
(h₁ : a ∈ s)
(h₂ : s.max = ↑b) :
a ≤ b
theorem
finset.not_mem_of_max_lt
{α : Type u_2}
[linear_order α]
{s : finset α}
{a b : α}
(h₁ : b < a)
(h₂ : s.max = ↑b) :
a ∉ s
@[protected]
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 with_top α. If you want to get an element of α, see
s.min'.
@[simp]
theorem
finset.min_insert
{α : Type u_2}
[linear_order α]
{a : α}
{s : finset α} :
(has_insert.insert a s).min = linear_order.min ↑a s.min
theorem
finset.not_mem_of_coe_lt_min
{α : Type u_2}
[linear_order α]
{a : α}
{s : finset α}
(h : ↑a < s.min) :
a ∉ s
theorem
finset.min_le_of_eq
{α : Type u_2}
[linear_order α]
{s : finset α}
{a b : α}
(h₁ : b ∈ s)
(h₂ : s.min = ↑a) :
a ≤ b
theorem
finset.not_mem_of_lt_min
{α : Type u_2}
[linear_order α]
{s : finset α}
{a b : α}
(h₁ : a < b)
(h₂ : s.min = ↑b) :
a ∉ 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 with_top α.
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 with_bot α.
@[simp]
{a}.min' _ is a.
theorem
finset.is_greatest_max'
{α : Type u_2}
[linear_order α]
(s : finset α)
(H : s.nonempty) :
is_greatest ↑s (s.max' H)
@[simp]
{a}.max' _ is a.
theorem
finset.min'_lt_max'_of_card
{α : Type u_2}
[linear_order α]
(s : finset α)
(h₂ : 1 < s.card) :
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.of_dual_min'
{α : Type u_2}
[linear_order α]
{s : finset αᵒᵈ}
(hs : s.nonempty) :
⇑order_dual.of_dual (s.min' hs) = (finset.image ⇑order_dual.of_dual s).max' _
theorem
finset.of_dual_max'
{α : Type u_2}
[linear_order α]
{s : finset αᵒᵈ}
(hs : s.nonempty) :
⇑order_dual.of_dual (s.max' hs) = (finset.image ⇑order_dual.of_dual s).min' _
theorem
finset.to_dual_min'
{α : Type u_2}
[linear_order α]
{s : finset α}
(hs : s.nonempty) :
⇑order_dual.to_dual (s.min' hs) = (finset.image ⇑order_dual.to_dual s).max' _
theorem
finset.to_dual_max'
{α : Type u_2}
[linear_order α]
{s : finset α}
(hs : s.nonempty) :
⇑order_dual.to_dual (s.max' hs) = (finset.image ⇑order_dual.to_dual s).min' _
theorem
finset.max'_subset
{α : Type u_2}
[linear_order α]
{s t : finset α}
(H : s.nonempty)
(hst : s ⊆ t) :
theorem
finset.min'_subset
{α : Type u_2}
[linear_order α]
{s t : finset α}
(H : s.nonempty)
(hst : s ⊆ t) :
theorem
finset.max'_insert
{α : Type u_2}
[linear_order α]
(a : α)
(s : finset α)
(H : s.nonempty) :
(has_insert.insert a s).max' _ = linear_order.max (s.max' H) a
theorem
finset.min'_insert
{α : Type u_2}
[linear_order α]
(a : α)
(s : finset α)
(H : s.nonempty) :
(has_insert.insert a s).min' _ = linear_order.min (s.min' H) a
theorem
finset.lt_max'_of_mem_erase_max'
{α : Type u_2}
[linear_order α]
(s : finset α)
(H : s.nonempty)
[decidable_eq α]
{a : α}
(ha : a ∈ s.erase (s.max' H)) :
theorem
finset.min'_lt_of_mem_erase_min'
{α : Type u_2}
[linear_order α]
(s : finset α)
(H : s.nonempty)
[decidable_eq α]
{a : α}
(ha : a ∈ s.erase (s.min' H)) :
@[simp]
theorem
finset.max'_image
{α : Type u_2}
{β : Type u_3}
[linear_order α]
[linear_order β]
{f : α → β}
(hf : monotone f)
(s : finset α)
(h : (finset.image f s).nonempty) :
(finset.image f s).max' h = f (s.max' _)
@[simp]
theorem
finset.min'_image
{α : Type u_2}
{β : Type u_3}
[linear_order α]
[linear_order β]
{f : α → β}
(hf : monotone f)
(s : finset α)
(h : (finset.image f s).nonempty) :
(finset.image f s).min' h = f (s.min' _)
theorem
finset.max_mem_image_coe
{α : Type u_2}
[linear_order α]
{s : finset α}
(hs : s.nonempty) :
s.max ∈ finset.image coe s
theorem
finset.min_mem_image_coe
{α : Type u_2}
[linear_order α]
{s : finset α}
(hs : s.nonempty) :
s.min ∈ finset.image coe s
theorem
finset.max_mem_insert_bot_image_coe
{α : Type u_2}
[linear_order α]
(s : finset α) :
s.max ∈ has_insert.insert ⊥ (finset.image coe s)
theorem
finset.min_mem_insert_top_image_coe
{α : Type u_2}
[linear_order α]
(s : finset α) :
s.min ∈ has_insert.insert ⊤ (finset.image coe s)
theorem
finset.max'_erase_ne_self
{α : Type u_2}
[linear_order α]
{x : α}
{s : finset α}
(s0 : (s.erase x).nonempty) :
theorem
finset.min'_erase_ne_self
{α : Type u_2}
[linear_order α]
{x : α}
{s : finset α}
(s0 : (s.erase x).nonempty) :
theorem
finset.card_le_diff_of_interleaved
{α : Type u_2}
[linear_order α]
{s t : finset α}
(h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → (∀ (z : α), z ∈ s → z ∉ set.Ioo x y) → (∃ (z : α) (H : z ∈ t), x < z ∧ z < y)) :
If finsets s and t are interleaved, then finset.card s ≤ finset.card (t \ s) + 1.
theorem
finset.induction_on_max
{α : Type u_2}
[linear_order α]
[decidable_eq α]
{p : finset α → Prop}
(s : finset α)
(h0 : p ∅)
(step : ∀ (a : α) (s : finset α), (∀ (x : α), x ∈ s → x < a) → p s → p (has_insert.insert a s)) :
p s
Induction principle for finsets in a linearly ordered type: a predicate is true on all
s : finset α provided that:
theorem
finset.induction_on_min
{α : Type u_2}
[linear_order α]
[decidable_eq α]
{p : finset α → Prop}
(s : finset α)
(h0 : p ∅)
(step : ∀ (a : α) (s : finset α), (∀ (x : α), x ∈ s → a < x) → p s → p (has_insert.insert a s)) :
p s
Induction principle for finsets in a linearly ordered type: a predicate is true on all
s : finset α provided that:
theorem
finset.induction_on_max_value
{α : Type u_2}
{ι : Type u_5}
[linear_order α]
[decidable_eq ι]
(f : ι → α)
{p : finset ι → Prop}
(s : finset ι)
(h0 : p ∅)
(step : ∀ (a : ι) (s : finset ι), a ∉ s → (∀ (x : ι), x ∈ s → f x ≤ f a) → p s → p (has_insert.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:
theorem
finset.induction_on_min_value
{α : Type u_2}
{ι : Type u_5}
[linear_order α]
[decidable_eq ι]
(f : ι → α)
{p : finset ι → Prop}
(s : finset ι)
(h0 : p ∅)
(step : ∀ (a : ι) (s : finset ι), a ∉ s → (∀ (x : ι), x ∈ s → f a ≤ f x) → p s → p (has_insert.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:
theorem
finset.is_lub_iff_is_greatest
{α : Type u_2}
[linear_order α]
(i : α)
(s : finset α)
(hs : s.nonempty) :
is_lub ↑s i ↔ is_greatest ↑s i
theorem
finset.is_glb_mem
{α : Type u_2}
[linear_order α]
{i : α}
(s : finset α)
(his : is_glb ↑s i)
(hs : s.nonempty) :
i ∈ s
theorem
finset.is_lub_mem
{α : Type u_2}
[linear_order α]
{i : α}
(s : finset α)
(his : is_lub ↑s i)
(hs : s.nonempty) :
i ∈ s
theorem
multiset.map_finset_sup
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[decidable_eq α]
[decidable_eq β]
(s : finset γ)
(f : γ → multiset β)
(g : β → α)
(hg : function.injective g) :
multiset.map g (s.sup f) = s.sup (multiset.map g ∘ f)
theorem
multiset.count_finset_sup
{α : Type u_2}
{β : Type u_3}
[decidable_eq β]
(s : finset α)
(f : α → multiset β)
(b : β) :
multiset.count b (s.sup f) = s.sup (λ (a : α), multiset.count b (f a))
@[simp]
theorem
finset.sup_singleton''
{α : Type u_2}
{β : Type u_3}
[decidable_eq α]
(s : finset β)
(f : β → α) :
s.sup (λ (b : β), {f b}) = finset.image f s
@[simp]
Supremum of s i, i : ι, is equal to the supremum over t : finset ι of suprema
⨆ i ∈ t, s i. This version assumes ι is a Type*. See supr_eq_supr_finset' for a version
that works for ι : Sort*.
Supremum of s i, i : ι, is equal to the supremum over t : finset ι of suprema
⨆ i ∈ t, s i. This version works for ι : Sort*. See supr_eq_supr_finset for a version
that assumes ι : Type* but has no plifts.
Infimum of s i, i : ι, is equal to the infimum over t : finset ι of infima
⨅ i ∈ t, s i. This version assumes ι is a Type*. See infi_eq_infi_finset' for a version
that works for ι : Sort*.
Infimum of s i, i : ι, is equal to the infimum over t : finset ι of infima
⨅ i ∈ t, s i. This version works for ι : Sort*. See infi_eq_infi_finset for a version
that assumes ι : Type* but has no plifts.
Union of an indexed family of sets s : ι → 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.
Intersection of an indexed family of sets s : ι → 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*.
Intersection of an indexed family of sets s : ι → 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 #
Interaction with big lattice/set operations #
theorem
finset.supr_singleton
{α : Type u_2}
{β : Type u_3}
[complete_lattice β]
(a : α)
(s : α → β) :
theorem
finset.infi_singleton
{α : Type u_2}
{β : Type u_3}
[complete_lattice β]
(a : α)
(s : α → β) :
theorem
finset.supr_insert
{α : Type u_2}
{β : Type u_3}
[complete_lattice β]
[decidable_eq α]
(a : α)
(s : finset α)
(t : α → β) :
theorem
finset.infi_insert
{α : Type u_2}
{β : Type u_3}
[complete_lattice β]
[decidable_eq α]
(a : α)
(s : finset α)
(t : α → β) :
theorem
finset.supr_finset_image
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[complete_lattice β]
[decidable_eq α]
{f : γ → α}
{g : α → β}
{s : finset γ} :
theorem
finset.infi_finset_image
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[complete_lattice β]
[decidable_eq α]
{f : γ → α}
{g : α → β}
{s : finset γ} :
theorem
finset.supr_insert_update
{α : Type u_2}
{β : Type u_3}
[complete_lattice β]
[decidable_eq α]
{x : α}
{t : finset α}
(f : α → β)
{s : β}
(hx : x ∉ t) :
(⨆ (i : α) (H : i ∈ has_insert.insert x t), function.update f x s i) = s ⊔ ⨆ (i : α) (H : i ∈ t), f i
theorem
finset.infi_insert_update
{α : Type u_2}
{β : Type u_3}
[complete_lattice β]
[decidable_eq α]
{x : α}
{t : finset α}
(f : α → β)
{s : β}
(hx : x ∉ t) :
(⨅ (i : α) (H : i ∈ has_insert.insert x t), function.update f x s i) = s ⊓ ⨅ (i : α) (H : i ∈ t), f i
theorem
finset.set_bUnion_insert_update
{α : Type u_2}
{β : Type u_3}
[decidable_eq α]
{x : α}
{t : finset α}
(f : α → set β)
{s : set β}
(hx : x ∉ t) :
(⋃ (i : α) (H : i ∈ has_insert.insert x t), function.update f x s i) = s ∪ ⋃ (i : α) (H : i ∈ t), f i
theorem
finset.set_bInter_insert_update
{α : Type u_2}
{β : Type u_3}
[decidable_eq α]
{x : α}
{t : finset α}
(f : α → set β)
{s : set β}
(hx : x ∉ t) :
(⋂ (i : α) (H : i ∈ has_insert.insert x t), function.update f x s i) = s ∩ ⋂ (i : α) (H : i ∈ t), f i