optionIsSomeEquiv — Mathlib

English

The forward component of the constructed partial equivalence equals the given function f.

Русский

Передняя часть сконструированного частичного эквивалента равна заданной функции f.

LaTeX

$$$((\mathrm{PartialEquiv.mk}\ f\ g\ s\ t\ ml\ mr\ il\ ir) : \alpha \to \beta) = f$$$

Lean4

/-- The set of `x : Option α` such that `isSome x` is equivalent to `α`. -/
@[simps]
def optionIsSomeEquiv (α) : { x : Option α // x.isSome } ≃ α
    where
  toFun o := Option.get _ o.2
  invFun x := ⟨some x, rfl⟩
  left_inv _ := Subtype.eq <| Option.some_get _
  right_inv _ := Option.get_some _ _

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