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

instance Finset.instLocallyFiniteOrder {α : Type u_1} [DecidableEq α] : LocallyFiniteOrder (Finset α)

LocallyFiniteOrder instance for Finset α.

We provide an optimized definition for Finset.Icc (s : Finset α) t, then define the other intervals based on Icc.

We do not define, e.g., Finset.Ico based on Finset.ssubsets, because it would require more code without performance gain.

theorem Finset.Icc_eq_filter_powerset {α : Type u_1} [DecidableEq α] (s t : Finset α) : Icc s t = {u ∈ t.powerset | s ⊆ u}

theorem Finset.Ico_eq_filter_ssubsets {α : Type u_1} [DecidableEq α] (s t : Finset α) : Ico s t = {u ∈ t.ssubsets | s ⊆ u}

theorem Finset.Ioc_eq_filter_powerset {α : Type u_1} [DecidableEq α] (s t : Finset α) : Ioc s t = {u ∈ t.powerset | s ⊂ u}

theorem Finset.Ioo_eq_filter_ssubsets {α : Type u_1} [DecidableEq α] (s t : Finset α) : Ioo s t = {u ∈ t.ssubsets | s ⊂ u}

theorem Finset.Iic_eq_powerset {α : Type u_1} [DecidableEq α] (s : Finset α) : Iic s = s.powerset

theorem Finset.Iio_eq_ssubsets {α : Type u_1} [DecidableEq α] (s : Finset α) : Iio s = s.ssubsets

theorem Finset.Icc_eq_image_powerset {α : Type u_1} [DecidableEq α] {s t : Finset α} (h : s ⊆ t) : Icc s t = image (fun (x : Finset α) => s ∪ x) (t \ s).powerset

theorem Finset.Ico_eq_image_ssubsets {α : Type u_1} [DecidableEq α] {s t : Finset α} (h : s ⊆ t) : Ico s t = image (fun (x : Finset α) => s ∪ x) (t \ s).ssubsets

theorem Finset.card_Icc_finset {α : Type u_1} [DecidableEq α] {s t : Finset α} (h : s ⊆ t) : (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 t : Finset α} (h : s ⊆ t) : (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 t : Finset α} (h : s ⊆ t) : (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 t : Finset α} (h : s ⊆ t) : (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 α} : (Iic s).card = 2 ^ s.card

Cardinality of an Iic of finsets.

theorem Finset.card_Iio_finset {α : Type u_1} [DecidableEq α] {s : 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 : a ∉ s), f s ≤ f (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 : a ∉ s), f (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 : a ∉ s), f s < f (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 : a ∉ s), f (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 : α⦄, a ∉ s → f 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 : α⦄, a ∉ s → f (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 : α⦄, a ∉ s → f 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 : α⦄, a ∉ s → f (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.