powersetCardAux_zero

Mathlib.Data.Multiset.Powerset

URI: https://scilib.ai/kg/mathlib#Multiset.powersetCardAux_zero

English

s ∈ powersetCardAux n l iff s ≤ ↑l and card s = n.

Русский

s ∈ powersetCardAux n l тогда и только тогда, когда s ≤ ↑l и card s = n.

LaTeX

$$s ∈ \\mathrm{powersetCardAux}(n,l) \\iff (s \\le \\uparrow l) \\land \\mathrm{card}(s) = n$$

Lean4

@[simp]
theorem powersetCardAux_zero (l : List α) : powersetCardAux 0 l = [0] := by simp [powersetCardAux_eq_map_coe]

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

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

Разделы

Аффилиация

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