finTwoEquiv — Mathlib

English

There is a natural equivalence between Fin(2) and Bool, given by toFun(i) = (i = 1) and invFun(b) = if b then 1 else 0.

Русский

Существует естественная эквивалентность между Fin(2) и Bool: отображение toFun(i) = (i = 1) и обратное invFun(b) = если b то 1 иначе 0.

LaTeX

$$$\\mathrm{Fin}(2) \\cong \\mathrm{Bool}$$$

Lean4

/-- Equivalence between `Fin 2` and `Bool`. -/
def finTwoEquiv : Fin 2 ≃ Bool where
  toFun i := i == 1
  invFun b := bif b then 1 else 0
  left_inv i := by grind
  right_inv b := by grind

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