mathlib3 documentation

data.finset.interval

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

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) :
theorem finset.Ico_eq_image_ssubsets {α : Type u_1} [decidable_eq α] {s t : finset α} (h : s t) :
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.

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.

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.

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.

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

Cardinality of an Iic of finsets.

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.