Documentation

Mathlib.Data.Finset.Interval

Intervals of finsets as finsets #

This file provides the LocallyFiniteOrder instance for Finset α and calculates the cardinality of finite intervals of finsets.

If s t : Finset α, then Finset.Icc s t is the finset of finsets which include s and are included in t. For example, Finset.Icc {0, 1} {0, 1, 2, 3} = {{0, 1}, {0, 1, 2}, {0, 1, 3}, {0, 1, 2, 3}} and Finset.Icc {0, 1, 2} {0, 1, 3} = {}.

In addition, this file gives characterizations of monotone and strictly monotone functions out of Finset α in terms of Finset.insert

Equations
  • One or more equations did not get rendered due to their size.
theorem Finset.Icc_eq_filter_powerset {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) :
Finset.Icc s t = Finset.filter (fun (x : Finset α) => s x) t.powerset
theorem Finset.Ico_eq_filter_ssubsets {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) :
Finset.Ico s t = Finset.filter (fun (x : Finset α) => s x) t.ssubsets
theorem Finset.Ioc_eq_filter_powerset {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) :
Finset.Ioc s t = Finset.filter (fun (x : Finset α) => s x) t.powerset
theorem Finset.Ioo_eq_filter_ssubsets {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) :
Finset.Ioo s t = Finset.filter (fun (x : Finset α) => s x) t.ssubsets
theorem Finset.Iic_eq_powerset {α : Type u_1} [DecidableEq α] (s : Finset α) :
Finset.Iic s = s.powerset
theorem Finset.Iio_eq_ssubsets {α : Type u_1} [DecidableEq α] (s : Finset α) :
Finset.Iio s = s.ssubsets
theorem Finset.Icc_eq_image_powerset {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} (h : s t) :
Finset.Icc s t = Finset.image (fun (x : Finset α) => s x) (t \ s).powerset
theorem Finset.Ico_eq_image_ssubsets {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} (h : s t) :
Finset.Ico s t = Finset.image (fun (x : Finset α) => s x) (t \ s).ssubsets
theorem Finset.card_Icc_finset {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} (h : s t) :
(Finset.Icc s t).card = 2 ^ (t.card - s.card)

Cardinality of a non-empty Icc of finsets.

theorem Finset.card_Ico_finset {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} (h : s t) :
(Finset.Ico s t).card = 2 ^ (t.card - s.card) - 1

Cardinality of an Ico of finsets.

theorem Finset.card_Ioc_finset {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} (h : s t) :
(Finset.Ioc s t).card = 2 ^ (t.card - s.card) - 1

Cardinality of an Ioc of finsets.

theorem Finset.card_Ioo_finset {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} (h : s t) :
(Finset.Ioo s t).card = 2 ^ (t.card - s.card) - 2

Cardinality of an Ioo of finsets.

theorem Finset.card_Iic_finset {α : Type u_1} [DecidableEq α] {s : Finset α} :
(Finset.Iic s).card = 2 ^ s.card

Cardinality of an Iic of finsets.

theorem Finset.card_Iio_finset {α : Type u_1} [DecidableEq α] {s : Finset α} :
(Finset.Iio s).card = 2 ^ s.card - 1

Cardinality of an Iio of finsets.

theorem Finset.monotone_iff_forall_le_cons {α : Type u_1} {β : Type u_2} [Preorder β] {f : Finset αβ} :
Monotone f ∀ (s : Finset α) ⦃a : α⦄ (ha : as), f s f (Finset.cons a s ha)

A function f from Finset α is monotone if and only if f s ≤ f (cons a s ha) for all s and a ∉ s.

theorem Finset.antitone_iff_forall_cons_le {α : Type u_1} {β : Type u_2} [Preorder β] {f : Finset αβ} :
Antitone f ∀ (s : Finset α) ⦃a : α⦄ (ha : as), f (Finset.cons a s ha) f s

A function f from Finset α is antitone if and only if f (cons a s ha) ≤ f s for all s and a ∉ s.

theorem Finset.strictMono_iff_forall_lt_cons {α : Type u_1} {β : Type u_2} [Preorder β] {f : Finset αβ} :
StrictMono f ∀ (s : Finset α) ⦃a : α⦄ (ha : as), f s < f (Finset.cons a s ha)

A function f from Finset α is strictly monotone if and only if f s < f (cons a s ha) for all s and a ∉ s.

theorem Finset.strictAnti_iff_forall_cons_lt {α : Type u_1} {β : Type u_2} [Preorder β] {f : Finset αβ} :
StrictAnti f ∀ (s : Finset α) ⦃a : α⦄ (ha : as), f (Finset.cons a s ha) < f s

A function f from Finset α is strictly antitone if and only if f (cons a s ha) < f s for all s and a ∉ s.

theorem Finset.monotone_iff_forall_le_insert {α : Type u_1} {β : Type u_2} [Preorder β] {f : Finset αβ} [DecidableEq α] :
Monotone f ∀ (s : Finset α) ⦃a : α⦄, asf s f (insert a s)

A function f from Finset α is monotone if and only if f s ≤ f (insert a s) for all s and a ∉ s.

theorem Finset.antitone_iff_forall_insert_le {α : Type u_1} {β : Type u_2} [Preorder β] {f : Finset αβ} [DecidableEq α] :
Antitone f ∀ (s : Finset α) ⦃a : α⦄, asf (insert a s) f s

A function f from Finset α is antitone if and only if f (insert a s) ≤ f s for all s and a ∉ s.

theorem Finset.strictMono_iff_forall_lt_insert {α : Type u_1} {β : Type u_2} [Preorder β] {f : Finset αβ} [DecidableEq α] :
StrictMono f ∀ (s : Finset α) ⦃a : α⦄, asf s < f (insert a s)

A function f from Finset α is strictly monotone if and only if f s < f (insert a s) for all s and a ∉ s.

theorem Finset.strictAnti_iff_forall_lt_insert {α : Type u_1} {β : Type u_2} [Preorder β] {f : Finset αβ} [DecidableEq α] :
StrictAnti f ∀ (s : Finset α) ⦃a : α⦄, asf (insert a s) < f s

A function f from Finset α is strictly antitone if and only if f (insert a s) < f s for all s and a ∉ s.