down — Mathlib

English

There is a canonical equivalence between the semiring of subsets of a type α and the power set of α, given by the identity correspondence.

Русский

Существует каноническое эквивалентное отображение между полем множеств SetSemiring α и множеством всех подмножеств α, заданное тождественным отображением.

LaTeX

$$$SetSemiring \alpha \simeq Set \alpha$$$

Lean4

/-- The identity function `SetSemiring α → Set α`. -/
protected def down : SetSemiring α ≃ Set α :=
  Equiv.refl _

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