setPreimage_id — Mathlib

English

Let α be a type. The preimage map along the identity on α coincides with the identity map on the lattice of subsets of α.

Русский

Пусть α — множество. Предобразность по тождественной функции на α совпадает с тождественным отображением на множество подмножеств α.

LaTeX

$$$$ \operatorname{setPreimage}(\mathrm{id}_{\alpha}) = \mathrm{id}_{\mathcal{P}(\alpha)}. $$$$

Lean4

@[simp]
theorem setPreimage_id : setPreimage (id : α → α) = CompleteLatticeHom.id _ :=
  rfl

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