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.instLocallyFiniteOrderFinsetToPreorderPartialOrder {α : Type u_1} [DecidableEq α] : LocallyFiniteOrder (Finset α)

theorem Finset.Icc_eq_filter_powerset {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) : Finset.Icc s t = Finset.filter ((fun x x_1 => x ⊆ x_1) s) (Finset.powerset t)

theorem Finset.Ico_eq_filter_ssubsets {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) : Finset.Ico s t = Finset.filter ((fun x x_1 => x ⊆ x_1) s) (Finset.ssubsets t)

theorem Finset.Ioc_eq_filter_powerset {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) : Finset.Ioc s t = Finset.filter ((fun x x_1 => x ⊂ x_1) s) (Finset.powerset t)

theorem Finset.Ioo_eq_filter_ssubsets {α : Type u_1} [DecidableEq α] (s : Finset α) (t : Finset α) : Finset.Ioo s t = Finset.filter ((fun x x_1 => x ⊂ x_1) s) (Finset.ssubsets t)

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

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

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 x_1 => x ∪ x_1) s) (Finset.powerset (t \ s))

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 x_1 => x ∪ x_1) s) (Finset.ssubsets (t \ s))

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

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.card (Finset.Ico s t) = 2 ^ (Finset.card t - Finset.card s) - 1

Cardinality of an Ico of finsets.

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

Cardinality of an Ioc of finsets.

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

Cardinality of an Ioo of finsets.

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

Cardinality of an Iic of finsets.

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

Cardinality of an Iio of finsets.

theorem Finset.covby_cons {α : Type u_1} {s : Finset α} {i : α} (hi : ¬i ∈ s) : s ⋖ Finset.cons i s hi

theorem Finset.covby_iff {α : Type u_1} {s : Finset α} {t : Finset α} : s ⋖ t ↔ ∃ i hi, t = Finset.cons i s hi

theorem Finset.monotone_iff {α : Type u_1} {β : Type u_2} [Preorder β] (f : Finset α → β) : Monotone f ↔ ∀ (s : Finset α) {i : α} (hi : ¬i ∈ s), f s ≤ f (Finset.cons i s hi)

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

theorem Finset.strictMono_iff {α : Type u_1} {β : Type u_2} [Preorder β] (f : Finset α → β) : StrictMono f ↔ ∀ (s : Finset α) {i : α} (hi : ¬i ∈ s), f s < f (Finset.cons i s hi)

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

theorem Finset.antitone_iff {α : Type u_1} {β : Type u_2} [Preorder β] (f : Finset α → β) : Antitone f ↔ ∀ (s : Finset α) {i : α} (hi : ¬i ∈ s), f (Finset.cons i s hi) ≤ f s

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

theorem Finset.strictAnti_iff {α : Type u_1} {β : Type u_2} [Preorder β] (f : Finset α → β) : StrictAnti f ↔ ∀ (s : Finset α) {i : α} (hi : ¬i ∈ s), f (Finset.cons i s hi) < f s

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

theorem Finset.covby_insert {α : Type u_1} {s : Finset α} [DecidableEq α] {i : α} (hi : ¬i ∈ s) : s ⋖ insert i s

theorem Finset.covby_iff' {α : Type u_1} {s : Finset α} {t : Finset α} [DecidableEq α] : s ⋖ t ↔ ∃ i, ¬i ∈ s ∧ t = insert i s

theorem Finset.monotone_iff' {α : Type u_1} [DecidableEq α] {β : Type u_2} [Preorder β] (f : Finset α → β) : Monotone f ↔ ∀ (s : Finset α) {i : α}, ¬i ∈ s → f s ≤ f (insert i s)

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

theorem Finset.strictMono_iff' {α : Type u_1} [DecidableEq α] {β : Type u_2} [Preorder β] (f : Finset α → β) : StrictMono f ↔ ∀ (s : Finset α) {i : α}, ¬i ∈ s → f s < f (insert i s)

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

theorem Finset.antitone_iff' {α : Type u_1} [DecidableEq α] {β : Type u_2} [Preorder β] (f : Finset α → β) : Antitone f ↔ ∀ (s : Finset α) {i : α}, ¬i ∈ s → f (insert i s) ≤ f s

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

theorem Finset.strictAnti_iff' {α : Type u_1} [DecidableEq α] {β : Type u_2} [Preorder β] (f : Finset α → β) : StrictAnti f ↔ ∀ (s : Finset α) {i : α}, ¬i ∈ s → f (insert i s) < f s

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