propEquivBool — Mathlib

English

The type Prop is noncomputably equivalent to Bool; there exists a noncomputable Equiv Prop Bool.

Русский

Тип Prop не вычислительно эквивалентен Bool; существует невычислимое эквивалентность Prop Bool.

LaTeX

$$$ \operatorname{Prop} \simeq \operatorname{Bool} $$$

Lean4

/-- `Prop` is noncomputably equivalent to `Bool`. -/
noncomputable def propEquivBool : Prop ≃ Bool
    where
  toFun p := @decide p (Classical.propDecidable _)
  invFun b := b
  left_inv p := by simp
  right_inv b := by simp

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