powerset_singleton — Mathlib

English

For any a, the set of all pairs with first coordinate a is equal to {a} × β, i.e., fst^{-1}({a}) = {a} × β.

Русский

Для любого a множество пар с первой компонентой a равно {a} × β, т.е. fst^{-1}({a}) = {a} × β.

LaTeX

$$$\\mathrm{fst}^{-1}(\\{a\\}) = \\{a\\} \\times \\beta$$$

Lean4

/-- The powerset of a singleton contains only `∅` and the singleton itself. -/
theorem powerset_singleton (x : α) : 𝒫({ x } : Set α) = {∅, { x }} := by grind

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