# mathlibdocumentation

data.finset.interval

# Intervals of finsets as finsets #

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} = {}.

@[protected, instance]
def finset.locally_finite_order {α : Type u_1} [decidable_eq α] :
Equations
theorem finset.Icc_eq_filter_powerset {α : Type u_1} [decidable_eq α] (s t : finset α) :
theorem finset.Ico_eq_filter_ssubsets {α : Type u_1} [decidable_eq α] (s t : finset α) :
theorem finset.Ioc_eq_filter_powerset {α : Type u_1} [decidable_eq α] (s t : finset α) :
theorem finset.Ioo_eq_filter_ssubsets {α : Type u_1} [decidable_eq α] (s t : finset α) :
theorem finset.Iic_eq_powerset {α : Type u_1} [decidable_eq α] (s : finset α) :
theorem finset.Iio_eq_ssubsets {α : Type u_1} [decidable_eq α] (s : finset α) :
theorem finset.Icc_eq_image_powerset {α : Type u_1} [decidable_eq α] {s t : finset α} (h : s t) :
t = (t \ s).powerset
theorem finset.Ico_eq_image_ssubsets {α : Type u_1} [decidable_eq α] {s t : finset α} (h : s t) :
t = (t \ s).ssubsets
theorem finset.card_Icc_finset {α : Type u_1} [decidable_eq α] {s t : finset α} (h : s t) :
t).card = 2 ^ (t.card - s.card)

Cardinality of a non-empty Icc of finsets.

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

Cardinality of an Ico of finsets.

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

Cardinality of an Ioc of finsets.

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

Cardinality of an Ioo of finsets.