Iic_eq_powerset — Mathlib

English

For any finite set s, the lower interval Iic(s) consists of all subsets of s, i.e., the powerset of s.

Русский

Для любого конечного множества s нижний интервал Iic(s) состоит из всех подмножеств s, то есть это множество подмножеств s (повероятный набор).

LaTeX

$$$Iic(s) = \\mathcal{P}(s)$$$

Lean4

theorem Iic_eq_powerset : Iic s = s.powerset := by ext; simp

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