Lattice operations on finsets #
sup #
def
finset.sup
{α : Type u_1}
{β : Type u_2}
[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
theorem
finset.sup_def
{α : Type u_1}
{β : Type u_2}
[semilattice_sup α]
[order_bot α]
{s : finset β}
{f : β → α} :
s.sup f = (multiset.map f s.val).sup
@[simp]
theorem
finset.sup_empty
{α : Type u_1}
{β : Type u_2}
[semilattice_sup α]
[order_bot α]
{f : β → α} :
@[simp]
theorem
finset.sup_cons
{α : Type u_1}
{β : Type u_2}
[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_1}
{β : Type u_2}
[semilattice_sup α]
[order_bot α]
{s : finset β}
{f : β → α}
[decidable_eq β]
{b : β} :
theorem
finset.sup_image
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[semilattice_sup α]
[order_bot α]
[decidable_eq β]
(s : finset γ)
(f : γ → β)
(g : β → α) :
(finset.image f s).sup g = s.sup (g ∘ f)
@[simp]
theorem
finset.sup_map
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[semilattice_sup α]
[order_bot α]
(s : finset γ)
(f : γ ↪ β)
(g : β → α) :
@[simp]
theorem
finset.sup_singleton
{α : Type u_1}
{β : Type u_2}
[semilattice_sup α]
[order_bot α]
{f : β → α}
{b : β} :
theorem
finset.sup_union
{α : Type u_1}
{β : Type u_2}
[semilattice_sup α]
[order_bot α]
{s₁ s₂ : finset β}
{f : β → α}
[decidable_eq β] :
@[simp]
theorem
finset.sup_le_iff
{α : Type u_1}
{β : Type u_2}
[semilattice_sup α]
[order_bot α]
{s : finset β}
{f : β → α}
{a : α} :
@[simp]
theorem
finset.sup_bUnion
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[semilattice_sup α]
[order_bot α]
{f : β → α}
[decidable_eq β]
(s : finset γ)
(t : γ → finset β) :
theorem
finset.sup_const
{α : Type u_1}
{β : Type u_2}
[semilattice_sup α]
[order_bot α]
{s : finset β}
(h : s.nonempty)
(c : α) :
@[simp]
theorem
finset.sup_bot
{α : Type u_1}
{β : Type u_2}
[semilattice_sup α]
[order_bot α]
(s : finset β) :
theorem
finset.sup_ite
{α : Type u_1}
{β : Type u_2}
[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
theorem
finset.sup_le
{α : Type u_1}
{β : Type u_2}
[semilattice_sup α]
[order_bot α]
{s : finset β}
{f : β → α}
{a : α} :
theorem
finset.le_sup
{α : Type u_1}
{β : Type u_2}
[semilattice_sup α]
[order_bot α]
{s : finset β}
{f : β → α}
{b : β}
(hb : b ∈ s) :
theorem
finset.sup_mono_fun
{α : Type u_1}
{β : Type u_2}
[semilattice_sup α]
[order_bot α]
{s : finset β}
{f g : β → α}
(h : ∀ (b : β), b ∈ s → f b ≤ g b) :
theorem
finset.sup_mono
{α : Type u_1}
{β : Type u_2}
[semilattice_sup α]
[order_bot α]
{s₁ s₂ : finset β}
{f : β → α}
(h : s₁ ⊆ s₂) :
theorem
finset.sup_product_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[semilattice_sup α]
[order_bot α]
(s : finset β)
(t : finset γ)
(f : β × γ → α) :
See also finset.product_bUnion.
@[simp]
theorem
finset.sup_erase_bot
{α : Type u_1}
[semilattice_sup α]
[order_bot α]
[decidable_eq α]
(s : finset α) :
theorem
finset.sup_sdiff_right
{α : Type u_1}
{β : Type u_2}
[generalized_boolean_algebra α]
(s : finset β)
(f : β → α)
(a : α) :
theorem
finset.sup_coe
{α : Type u_1}
{β : Type u_2}
[semilattice_sup α]
[order_bot α]
{P : α → Prop}
{Pbot : P ⊥}
{Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)}
(t : finset β)
(f : β → {x // P x}) :
Computing sup in a subtype (closed under sup) is the same as computing it in α.
@[simp]
theorem
finset.sup_to_finset
{α : Type u_1}
{β : Type u_2}
[decidable_eq β]
(s : finset α)
(f : α → multiset β) :
theorem
finset.sup_induction
{α : Type u_1}
{β : Type u_2}
[semilattice_sup α]
[order_bot α]
{s : finset β}
{f : β → α}
{p : α → Prop}
(hb : p ⊥)
(hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂))
(hs : ∀ (b : β), b ∈ s → p (f b)) :
p (s.sup f)
theorem
finset.sup_eq_supr
{α : Type u_1}
{β : Type u_2}
[complete_lattice β]
(s : finset α)
(f : α → β) :
theorem
finset.sup_eq_Sup_image
{α : Type u_1}
{β : Type u_2}
[complete_lattice β]
(s : finset α)
(f : α → β) :
inf #
def
finset.inf
{α : Type u_1}
{β : Type u_2}
[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_1}
{β : Type u_2}
[semilattice_inf α]
[order_top α]
{s : finset β}
{f : β → α} :
s.inf f = (multiset.map f s.val).inf
@[simp]
theorem
finset.inf_empty
{α : Type u_1}
{β : Type u_2}
[semilattice_inf α]
[order_top α]
{f : β → α} :
@[simp]
theorem
finset.inf_cons
{α : Type u_1}
{β : Type u_2}
[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_1}
{β : Type u_2}
[semilattice_inf α]
[order_top α]
{s : finset β}
{f : β → α}
[decidable_eq β]
{b : β} :
theorem
finset.inf_image
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[semilattice_inf α]
[order_top α]
[decidable_eq β]
(s : finset γ)
(f : γ → β)
(g : β → α) :
(finset.image f s).inf g = s.inf (g ∘ f)
@[simp]
theorem
finset.inf_map
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[semilattice_inf α]
[order_top α]
(s : finset γ)
(f : γ ↪ β)
(g : β → α) :
@[simp]
theorem
finset.inf_singleton
{α : Type u_1}
{β : Type u_2}
[semilattice_inf α]
[order_top α]
{f : β → α}
{b : β} :
theorem
finset.inf_union
{α : Type u_1}
{β : Type u_2}
[semilattice_inf α]
[order_top α]
{s₁ s₂ : finset β}
{f : β → α}
[decidable_eq β] :
@[simp]
theorem
finset.inf_bUnion
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[semilattice_inf α]
[order_top α]
{f : β → α}
[decidable_eq β]
(s : finset γ)
(t : γ → finset β) :
theorem
finset.inf_const
{α : Type u_1}
{β : Type u_2}
[semilattice_inf α]
[order_top α]
{s : finset β}
(h : s.nonempty)
(c : α) :
@[simp]
theorem
finset.inf_top
{α : Type u_1}
{β : Type u_2}
[semilattice_inf α]
[order_top α]
(s : finset β) :
theorem
finset.le_inf_iff
{α : Type u_1}
{β : Type u_2}
[semilattice_inf α]
[order_top α]
{s : finset β}
{f : β → α}
{a : α} :
theorem
finset.inf_le
{α : Type u_1}
{β : Type u_2}
[semilattice_inf α]
[order_top α]
{s : finset β}
{f : β → α}
{b : β}
(hb : b ∈ s) :
theorem
finset.le_inf
{α : Type u_1}
{β : Type u_2}
[semilattice_inf α]
[order_top α]
{s : finset β}
{f : β → α}
{a : α} :
theorem
finset.inf_mono_fun
{α : Type u_1}
{β : Type u_2}
[semilattice_inf α]
[order_top α]
{s : finset β}
{f g : β → α}
(h : ∀ (b : β), b ∈ s → f b ≤ g b) :
theorem
finset.inf_mono
{α : Type u_1}
{β : Type u_2}
[semilattice_inf α]
[order_top α]
{s₁ s₂ : finset β}
{f : β → α}
(h : s₁ ⊆ s₂) :
@[simp]
theorem
finset.inf_erase_top
{α : Type u_1}
[semilattice_inf α]
[order_top α]
[decidable_eq α]
(s : finset α) :
theorem
finset.sup_sdiff_left
{α : Type u_1}
{β : Type u_2}
[boolean_algebra α]
(s : finset β)
(f : β → α)
(a : α) :
theorem
finset.inf_sdiff_left
{α : Type u_1}
{β : Type u_2}
[boolean_algebra α]
{s : finset β}
(hs : s.nonempty)
(f : β → α)
(a : α) :
theorem
finset.inf_sdiff_right
{α : Type u_1}
{β : Type u_2}
[boolean_algebra α]
{s : finset β}
(hs : s.nonempty)
(f : β → α)
(a : α) :
theorem
finset.inf_coe
{α : Type u_1}
{β : Type u_2}
[semilattice_inf α]
[order_top α]
{P : α → Prop}
{Ptop : P ⊤}
{Pinf : ∀ ⦃x y : α⦄, P x → P y → P (x ⊓ y)}
(t : finset β)
(f : β → {x // P x}) :
Computing inf in a subtype (closed under inf) is the same as computing it in α.
theorem
finset.inf_induction
{α : Type u_1}
{β : Type u_2}
[semilattice_inf α]
[order_top α]
{s : finset β}
{f : β → α}
{p : α → Prop}
(ht : p ⊤)
(hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊓ a₂))
(hs : ∀ (b : β), b ∈ s → p (f b)) :
p (s.inf f)
theorem
finset.sup_inf_distrib_left
{α : Type u_1}
{ι : Type u_4}
[distrib_lattice α]
[order_bot α]
(s : finset ι)
(f : ι → α)
(a : α) :
theorem
finset.sup_inf_distrib_right
{α : Type u_1}
{ι : Type u_4}
[distrib_lattice α]
[order_bot α]
(s : finset ι)
(f : ι → α)
(a : α) :
theorem
finset.disjoint_sup_right
{α : Type u_1}
{β : Type u_2}
[distrib_lattice α]
[order_bot α]
{s : finset β}
{f : β → α}
{a : α} :
theorem
finset.disjoint_sup_left
{α : Type u_1}
{β : Type u_2}
[distrib_lattice α]
[order_bot α]
{s : finset β}
{f : β → α}
{a : α} :
theorem
finset.inf_sup_distrib_left
{α : Type u_1}
{ι : Type u_4}
[distrib_lattice α]
[order_top α]
(s : finset ι)
(f : ι → α)
(a : α) :
theorem
finset.inf_sup_distrib_right
{α : Type u_1}
{ι : Type u_4}
[distrib_lattice α]
[order_top α]
(s : finset ι)
(f : ι → α)
(a : α) :
theorem
finset.inf_eq_infi
{α : Type u_1}
{β : Type u_2}
[complete_lattice β]
(s : finset α)
(f : α → β) :
theorem
finset.inf_eq_Inf_image
{α : Type u_1}
{β : Type u_2}
[complete_lattice β]
(s : finset α)
(f : α → β) :
theorem
finset.sup_of_mem
{α : Type u_1}
{β : Type u_2}
[semilattice_sup α]
{s : finset β}
(f : β → α)
{b : β}
(h : b ∈ s) :
def
finset.sup'
{α : Type u_1}
{β : Type u_2}
[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.
Equations
- s.sup' H f = option.get _
- _ = _
@[simp]
theorem
finset.sup'_cons
{α : Type u_1}
{β : Type u_2}
[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_1}
{β : Type u_2}
[semilattice_sup α]
{s : finset β}
(H : s.nonempty)
(f : β → α)
[decidable_eq β]
{b : β}
{h : (insert b s).nonempty} :
@[simp]
theorem
finset.sup'_singleton
{α : Type u_1}
{β : Type u_2}
[semilattice_sup α]
(f : β → α)
{b : β}
{h : {b}.nonempty} :
theorem
finset.sup'_le
{α : Type u_1}
{β : Type u_2}
[semilattice_sup α]
{s : finset β}
(H : s.nonempty)
(f : β → α)
{a : α}
(hs : ∀ (b : β), b ∈ s → f b ≤ a) :
theorem
finset.le_sup'
{α : Type u_1}
{β : Type u_2}
[semilattice_sup α]
{s : finset β}
(f : β → α)
{b : β}
(h : b ∈ s) :
@[simp]
theorem
finset.sup'_const
{α : Type u_1}
{β : Type u_2}
[semilattice_sup α]
{s : finset β}
(H : s.nonempty)
(a : α) :
@[simp]
theorem
finset.sup'_le_iff
{α : Type u_1}
{β : Type u_2}
[semilattice_sup α]
{s : finset β}
(H : s.nonempty)
(f : β → α)
{a : α} :
theorem
finset.sup'_bUnion
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[semilattice_sup α]
(f : β → α)
[decidable_eq β]
{s : finset γ}
(Hs : s.nonempty)
{t : γ → finset β}
(Ht : ∀ (b : γ), (t b).nonempty) :
theorem
finset.comp_sup'_eq_sup'_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[semilattice_sup α]
[semilattice_sup γ]
{s : finset β}
(H : s.nonempty)
{f : β → α}
(g : α → γ)
(g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y) :
theorem
finset.sup'_induction
{α : Type u_1}
{β : Type u_2}
[semilattice_sup α]
{s : finset β}
(H : s.nonempty)
(f : β → α)
{p : α → Prop}
(hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂))
(hs : ∀ (b : β), b ∈ s → p (f b)) :
p (s.sup' H f)
theorem
finset.inf_of_mem
{α : Type u_1}
{β : Type u_2}
[semilattice_inf α]
{s : finset β}
(f : β → α)
{b : β}
(h : b ∈ s) :
def
finset.inf'
{α : Type u_1}
{β : Type u_2}
[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_1}
{β : Type u_2}
[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_1}
{β : Type u_2}
[semilattice_inf α]
{s : finset β}
(H : s.nonempty)
(f : β → α)
[decidable_eq β]
{b : β}
{h : (insert b s).nonempty} :
@[simp]
theorem
finset.inf'_singleton
{α : Type u_1}
{β : Type u_2}
[semilattice_inf α]
(f : β → α)
{b : β}
{h : {b}.nonempty} :
theorem
finset.le_inf'
{α : Type u_1}
{β : Type u_2}
[semilattice_inf α]
{s : finset β}
(H : s.nonempty)
(f : β → α)
{a : α}
(hs : ∀ (b : β), b ∈ s → a ≤ f b) :
theorem
finset.inf'_le
{α : Type u_1}
{β : Type u_2}
[semilattice_inf α]
{s : finset β}
(f : β → α)
{b : β}
(h : b ∈ s) :
@[simp]
theorem
finset.inf'_const
{α : Type u_1}
{β : Type u_2}
[semilattice_inf α]
{s : finset β}
(H : s.nonempty)
(a : α) :
@[simp]
theorem
finset.le_inf'_iff
{α : Type u_1}
{β : Type u_2}
[semilattice_inf α]
{s : finset β}
(H : s.nonempty)
(f : β → α)
{a : α} :
theorem
finset.inf'_bUnion
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[semilattice_inf α]
(f : β → α)
[decidable_eq β]
{s : finset γ}
(Hs : s.nonempty)
{t : γ → finset β}
(Ht : ∀ (b : γ), (t b).nonempty) :
theorem
finset.comp_inf'_eq_inf'_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[semilattice_inf α]
[semilattice_inf γ]
{s : finset β}
(H : s.nonempty)
{f : β → α}
(g : α → γ)
(g_inf : ∀ (x y : α), g (x ⊓ y) = g x ⊓ g y) :
theorem
finset.inf'_induction
{α : Type u_1}
{β : Type u_2}
[semilattice_inf α]
{s : finset β}
(H : s.nonempty)
(f : β → α)
{p : α → Prop}
(hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊓ a₂))
(hs : ∀ (b : β), b ∈ s → p (f b)) :
p (s.inf' H f)
theorem
finset.sup'_eq_sup
{α : Type u_1}
{β : Type u_2}
[semilattice_sup α]
[order_bot α]
{s : finset β}
(H : s.nonempty)
(f : β → α) :
theorem
finset.inf'_eq_inf
{α : Type u_1}
{β : Type u_2}
[semilattice_inf α]
[order_top α]
{s : finset β}
(H : s.nonempty)
(f : β → α) :
@[protected, simp]
theorem
finset.sup_apply
{α : Type u_1}
{β : Type u_2}
{C : β → Type u_5}
[Π (b : β), semilattice_sup (C b)]
[Π (b : β), order_bot (C b)]
(s : finset α)
(f : α → Π (b : β), C b)
(b : β) :
@[protected, simp]
theorem
finset.inf_apply
{α : Type u_1}
{β : Type u_2}
{C : β → Type u_5}
[Π (b : β), semilattice_inf (C b)]
[Π (b : β), order_top (C b)]
(s : finset α)
(f : α → Π (b : β), C b)
(b : β) :
@[protected, simp]
theorem
finset.sup'_apply
{α : Type u_1}
{β : Type u_2}
{C : β → Type u_5}
[Π (b : β), semilattice_sup (C b)]
{s : finset α}
(H : s.nonempty)
(f : α → Π (b : β), C b)
(b : β) :
@[protected, simp]
theorem
finset.inf'_apply
{α : Type u_1}
{β : Type u_2}
{C : β → Type u_5}
[Π (b : β), semilattice_inf (C b)]
{s : finset α}
(H : s.nonempty)
(f : α → Π (b : β), C b)
(b : β) :
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 none otherwise. It belongs to option α. If you want to get an element of α, see
s.max'.
Equations
@[simp]
@[simp]
theorem
finset.le_max_of_mem
{α : Type u_1}
[linear_order α]
{s : finset α}
{a b : α}
(h₁ : a ∈ s)
(h₂ : b ∈ s.max) :
a ≤ b
@[protected]
Let s be a finset in a linear order. Then s.min is the minimum of s if s is not empty,
and none otherwise. It belongs to option α. If you want to get an element of α, see
s.min'.
Equations
@[simp]
@[simp]
theorem
finset.min_le_of_mem
{α : Type u_1}
[linear_order α]
{s : finset α}
{a b : α}
(h₁ : b ∈ s)
(h₂ : a ∈ s.min) :
a ≤ b
theorem
finset.le_min'
{α : Type u_1}
[linear_order α]
(s : finset α)
(H : s.nonempty)
(x : α)
(H2 : ∀ (y : α), y ∈ s → x ≤ y) :
@[simp]
theorem
finset.le_min'_iff
{α : Type u_1}
[linear_order α]
(s : finset α)
(H : s.nonempty)
{x : α} :
@[simp]
{a}.min' _ is a.
theorem
finset.max'_le
{α : Type u_1}
[linear_order α]
(s : finset α)
(H : s.nonempty)
(x : α)
(H2 : ∀ (y : α), y ∈ s → y ≤ x) :
theorem
finset.is_greatest_max'
{α : Type u_1}
[linear_order α]
(s : finset α)
(H : s.nonempty) :
is_greatest ↑s (s.max' H)
@[simp]
theorem
finset.max'_le_iff
{α : Type u_1}
[linear_order α]
(s : finset α)
(H : s.nonempty)
{x : α} :
@[simp]
theorem
finset.max'_lt_iff
{α : Type u_1}
[linear_order α]
(s : finset α)
(H : s.nonempty)
{x : α} :
@[simp]
theorem
finset.lt_min'_iff
{α : Type u_1}
[linear_order α]
(s : finset α)
(H : s.nonempty)
{x : α} :
@[simp]
{a}.max' _ is a.
theorem
finset.min'_lt_max'
{α : Type u_1}
[linear_order α]
(s : finset α)
{i j : α}
(H1 : i ∈ s)
(H2 : j ∈ s)
(H3 : i ≠ j) :
theorem
finset.min'_lt_max'_of_card
{α : Type u_1}
[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.max'_eq_of_dual_min'
{α : Type u_1}
[linear_order α]
{s : finset α}
(hs : s.nonempty) :
s.max' hs = ⇑order_dual.of_dual ((finset.image ⇑order_dual.to_dual s).min' _)
theorem
finset.min'_eq_of_dual_max'
{α : Type u_1}
[linear_order α]
{s : finset α}
(hs : s.nonempty) :
s.min' hs = ⇑order_dual.of_dual ((finset.image ⇑order_dual.to_dual s).max' _)
@[simp]
theorem
finset.of_dual_max_eq_min_of_dual
{α : Type u_1}
[linear_order α]
{a b : α} :
⇑order_dual.of_dual (max a b) = min (⇑order_dual.of_dual a) (⇑order_dual.of_dual b)
@[simp]
theorem
finset.of_dual_min_eq_max_of_dual
{α : Type u_1}
[linear_order α]
{a b : α} :
⇑order_dual.of_dual (min a b) = max (⇑order_dual.of_dual a) (⇑order_dual.of_dual b)
theorem
finset.max'_subset
{α : Type u_1}
[linear_order α]
{s t : finset α}
(H : s.nonempty)
(hst : s ⊆ t) :
theorem
finset.min'_subset
{α : Type u_1}
[linear_order α]
{s t : finset α}
(H : s.nonempty)
(hst : s ⊆ t) :
theorem
finset.max'_insert
{α : Type u_1}
[linear_order α]
(a : α)
(s : finset α)
(H : s.nonempty) :
theorem
finset.min'_insert
{α : Type u_1}
[linear_order α]
(a : α)
(s : finset α)
(H : s.nonempty) :
theorem
finset.lt_max'_of_mem_erase_max'
{α : Type u_1}
[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_1}
[linear_order α]
(s : finset α)
(H : s.nonempty)
[decidable_eq α]
{a : α}
(ha : a ∈ s.erase (s.min' H)) :
@[simp]
theorem
finset.max'_image
{α : Type u_1}
{β : Type u_2}
[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_1}
{β : Type u_2}
[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.induction_on_max
{α : Type u_1}
[linear_order α]
[decidable_eq α]
{p : finset α → Prop}
(s : finset α)
(h0 : p ∅)
(step : ∀ (a : α) (s : finset α), (∀ (x : α), x ∈ s → x < a) → p s → p (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_1}
[linear_order α]
[decidable_eq α]
{p : finset α → Prop}
(s : finset α)
(h0 : p ∅)
(step : ∀ (a : α) (s : finset α), (∀ (x : α), x ∈ s → a < x) → p s → p (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_1}
{ι : Type u_4}
[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 (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_1}
{ι : Type u_4}
[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 (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.exists_max_image
{α : Type u_1}
{β : Type u_2}
[linear_order α]
(s : finset β)
(f : β → α)
(h : s.nonempty) :
theorem
finset.exists_min_image
{α : Type u_1}
{β : Type u_2}
[linear_order α]
(s : finset β)
(f : β → α)
(h : s.nonempty) :
theorem
multiset.map_finset_sup
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[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_1}
{β : Type u_2}
[decidable_eq β]
(s : finset α)
(f : α → multiset β)
(b : β) :
multiset.count b (s.sup f) = s.sup (λ (a : α), multiset.count b (f a))
theorem
multiset.mem_sup
{α : Type u_1}
{β : Type u_2}
[decidable_eq β]
{s : finset α}
{f : α → multiset β}
{x : β} :
theorem
finset.mem_sup
{α : Type u_1}
{β : Type u_2}
[decidable_eq β]
{s : finset α}
{f : α → finset β}
{x : β} :
theorem
finset.sup_eq_bUnion
{α : Type u_1}
{β : Type u_2}
[decidable_eq β]
(s : finset α)
(t : α → finset β) :
@[simp]
theorem
finset.sup_singleton''
{α : Type u_1}
{β : Type u_2}
[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 assumes ι : Type*. See also Union_eq_Union_finset' for
a version that works for ι : Sort*.
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_1}
{β : Type u_2}
[complete_lattice β]
(a : α)
(s : α → β) :
theorem
finset.infi_singleton
{α : Type u_1}
{β : Type u_2}
[complete_lattice β]
(a : α)
(s : α → β) :
theorem
finset.supr_option_to_finset
{α : Type u_1}
{β : Type u_2}
[complete_lattice β]
(o : option α)
(f : α → β) :
theorem
finset.infi_option_to_finset
{α : Type u_1}
{β : Type u_2}
[complete_lattice β]
(o : option α)
(f : α → β) :
theorem
finset.supr_union
{α : Type u_1}
{β : Type u_2}
[complete_lattice β]
[decidable_eq α]
{f : α → β}
{s t : finset α} :
theorem
finset.infi_union
{α : Type u_1}
{β : Type u_2}
[complete_lattice β]
[decidable_eq α]
{f : α → β}
{s t : finset α} :
theorem
finset.supr_insert
{α : Type u_1}
{β : Type u_2}
[complete_lattice β]
[decidable_eq α]
(a : α)
(s : finset α)
(t : α → β) :
theorem
finset.infi_insert
{α : Type u_1}
{β : Type u_2}
[complete_lattice β]
[decidable_eq α]
(a : α)
(s : finset α)
(t : α → β) :
theorem
finset.supr_finset_image
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[complete_lattice β]
[decidable_eq α]
{f : γ → α}
{g : α → β}
{s : finset γ} :
(⨆ (x : α) (H : x ∈ finset.image f s), g x) = ⨆ (y : γ) (H : y ∈ s), g (f y)
theorem
finset.sup_finset_image
{α : Type u_1}
[decidable_eq α]
{β : Type u_2}
{γ : Type u_3}
[semilattice_sup β]
[order_bot β]
(f : γ → α)
(g : α → β)
(s : finset γ) :
(finset.image f s).sup g = s.sup (g ∘ f)
theorem
finset.infi_finset_image
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[complete_lattice β]
[decidable_eq α]
{f : γ → α}
{g : α → β}
{s : finset γ} :
(⨅ (x : α) (H : x ∈ finset.image f s), g x) = ⨅ (y : γ) (H : y ∈ s), g (f y)
theorem
finset.supr_insert_update
{α : Type u_1}
{β : Type u_2}
[complete_lattice β]
[decidable_eq α]
{x : α}
{t : finset α}
(f : α → β)
{s : β}
(hx : x ∉ t) :
theorem
finset.infi_insert_update
{α : Type u_1}
{β : Type u_2}
[complete_lattice β]
[decidable_eq α]
{x : α}
{t : finset α}
(f : α → β)
{s : β}
(hx : x ∉ t) :
theorem
finset.supr_bUnion
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[complete_lattice β]
[decidable_eq α]
(s : finset γ)
(t : γ → finset α)
(f : α → β) :
theorem
finset.infi_bUnion
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[complete_lattice β]
[decidable_eq α]
(s : finset γ)
(t : γ → finset α)
(f : α → β) :
theorem
finset.set_bUnion_insert
{α : Type u_1}
{β : Type u_2}
[decidable_eq α]
(a : α)
(s : finset α)
(t : α → set β) :
theorem
finset.set_bInter_insert
{α : Type u_1}
{β : Type u_2}
[decidable_eq α]
(a : α)
(s : finset α)
(t : α → set β) :
theorem
finset.set_bUnion_finset_image
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[decidable_eq α]
{f : γ → α}
{g : α → set β}
{s : finset γ} :
(⋃ (x : α) (H : x ∈ finset.image f s), g x) = ⋃ (y : γ) (H : y ∈ s), g (f y)
theorem
finset.set_bInter_finset_image
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[decidable_eq α]
{f : γ → α}
{g : α → set β}
{s : finset γ} :
(⋂ (x : α) (H : x ∈ finset.image f s), g x) = ⋂ (y : γ) (H : y ∈ s), g (f y)
theorem
finset.set_bUnion_insert_update
{α : Type u_1}
{β : Type u_2}
[decidable_eq α]
{x : α}
{t : finset α}
(f : α → set β)
{s : set β}
(hx : x ∉ t) :
theorem
finset.set_bInter_insert_update
{α : Type u_1}
{β : Type u_2}
[decidable_eq α]
{x : α}
{t : finset α}
(f : α → set β)
{s : set β}
(hx : x ∉ t) :