Intervals of finsets as finsets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file provides the locally_finite_order 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} = {}.

source

@[protected, instance]

def finset.locally_finite_order {α : Type u_1} [decidable_eq α] :

locally_finite_order (finset α)

Equations

finset.locally_finite_order = {finset_Icc := λ (s t : finset α), finset.filter (has_subset.subset s) t.powerset, finset_Ico := λ (s t : finset α), finset.filter (has_subset.subset s) t.ssubsets, finset_Ioc := λ (s t : finset α), finset.filter (has_ssubset.ssubset s) t.powerset, finset_Ioo := λ (s t : finset α), finset.filter (has_ssubset.ssubset s) t.ssubsets, finset_mem_Icc := _, finset_mem_Ico := _, finset_mem_Ioc := _, finset_mem_Ioo := _}

source

theorem finset.Icc_eq_filter_powerset {α : Type u_1} [decidable_eq α] (s t : finset α) :

finset.Icc s t = finset.filter (has_subset.subset s) t.powerset

source

theorem finset.Ico_eq_filter_ssubsets {α : Type u_1} [decidable_eq α] (s t : finset α) :

finset.Ico s t = finset.filter (has_subset.subset s) t.ssubsets

source

theorem finset.Ioc_eq_filter_powerset {α : Type u_1} [decidable_eq α] (s t : finset α) :

finset.Ioc s t = finset.filter (has_ssubset.ssubset s) t.powerset

source

theorem finset.Ioo_eq_filter_ssubsets {α : Type u_1} [decidable_eq α] (s t : finset α) :

finset.Ioo s t = finset.filter (has_ssubset.ssubset s) t.ssubsets

source

theorem finset.Iic_eq_powerset {α : Type u_1} [decidable_eq α] (s : finset α) :

finset.Iic s = s.powerset

source

theorem finset.Iio_eq_ssubsets {α : Type u_1} [decidable_eq α] (s : finset α) :

finset.Iio s = s.ssubsets

source

theorem finset.Icc_eq_image_powerset {α : Type u_1} [decidable_eq α] {s t : finset α} (h : s ⊆ t) :

finset.Icc s t = finset.image (has_union.union s) (t \ s).powerset

source

theorem finset.Ico_eq_image_ssubsets {α : Type u_1} [decidable_eq α] {s t : finset α} (h : s ⊆ t) :

finset.Ico s t = finset.image (has_union.union s) (t \ s).ssubsets

source

theorem finset.card_Icc_finset {α : Type u_1} [decidable_eq α] {s t : finset α} (h : s ⊆ t) :

(finset.Icc s t).card = 2 ^ (t.card - s.card)

Cardinality of a non-empty Icc of finsets.

source

theorem finset.card_Ico_finset {α : Type u_1} [decidable_eq α] {s t : finset α} (h : s ⊆ t) :

(finset.Ico s t).card = 2 ^ (t.card - s.card) - 1

Cardinality of an Ico of finsets.

source

theorem finset.card_Ioc_finset {α : Type u_1} [decidable_eq α] {s t : finset α} (h : s ⊆ t) :

(finset.Ioc s t).card = 2 ^ (t.card - s.card) - 1

Cardinality of an Ioc of finsets.

source

theorem finset.card_Ioo_finset {α : Type u_1} [decidable_eq α] {s t : finset α} (h : s ⊆ t) :

(finset.Ioo s t).card = 2 ^ (t.card - s.card) - 2

Cardinality of an Ioo of finsets.

source

theorem finset.card_Iic_finset {α : Type u_1} [decidable_eq α] {s : finset α} :

(finset.Iic s).card = 2 ^ s.card

Cardinality of an Iic of finsets.

source

theorem finset.card_Iio_finset {α : Type u_1} [decidable_eq α] {s : finset α} :

(finset.Iio s).card = 2 ^ s.card - 1

Cardinality of an Iio of finsets.