getRight_eq_getRight? — Mathlib

English

If h1 asserts x.isRight and h2 asserts x.getRight?.isSome, then x.getRight h1 = x.getRight?.get h2.

Русский

Если x является правой частью и естьSome для getRight?, то получаем равенство значений.

LaTeX

$$$\forall {x : \mathrm{Sum} \alpha \beta} (h_1 : x.isRight) (h_2 : x.getRight?.isSome),\ x.getRight h_1 = x.getRight?.get h_2$$

Lean4

theorem getRight_eq_getRight? (h₁ : x.isRight) (h₂ : x.getRight?.isSome) : x.getRight h₁ = x.getRight?.get h₂ := by
  simp [← getRight?_eq_some_iff]

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