sigmaOptionEquivOfSome — Mathlib

English

A sigma type over an Option with the none fiber empty is equivalent to a sigma type over the base type sans none.

Русский

Сигма-тип над Option с пустым ответвлением none эквивалентен сигма-типу над базовым типом без none.

LaTeX

$$$(\\Sigma x : \\mathrm{Option } \\alpha, p x) \\simeq \\Sigma x : \\alpha, p (\\mathrm{some } x)$, given h : p none → False$$

Lean4

/-- A sigma type over an `Option` is equivalent to the sigma set over the original type,
if the fiber is empty at none. -/
def sigmaOptionEquivOfSome {α} (p : Option α → Type v) (h : p none → False) :
    (Σ x : Option α, p x) ≃ Σ x : α, p (some x) :=
  haveI h' : ∀ x, p x → x.isSome := by
    intro x
    cases x
    · intro n
      exfalso
      exact h n
    · intro _
      exact rfl
  (sigmaSubtypeEquivOfSubset _ _ h').symm.trans (sigmaCongrLeft' (optionIsSomeEquiv α))

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