card_Iic_finset

Mathlib.Data.Finset.Interval

URI: https://scilib.ai/kg/mathlib#Finset.card_Iic_finset

English

The cardinality of the lower interval Iic(s) equals 2^(card(s)).

Русский

Кардинальность нижнего интервала Iic(s) равна 2^(card(s)).

LaTeX

$$(Iic s).card = 2^{s.card}$$

Lean4

/-- Cardinality of an `Iic` of finsets. -/
theorem card_Iic_finset : (Iic s).card = 2 ^ s.card := by rw [Iic_eq_powerset, card_powerset]

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru