isSome_getRight?_iff_isRight

Mathlib.Data.Sum.Basic

URI: https://scilib.ai/kg/mathlib#Sum.isSome_getRight?_iff_isRight

English

The getRight? option isSome is equivalent to the x isRight predicate (simp): x.getRight?.isSome ⇔ x.isRight.

Русский

Утверждение о том, что isSome у getRight? эквивалентно x.isRight.

LaTeX

$$@[simp]\n\text{theorem isSome_getRight?_iff_isRight} : x.getRight?.isSome \iff x.isRight$$

Lean4

@[simp]
theorem isSome_getRight?_iff_isRight : x.getRight?.isSome ↔ x.isRight := by rw [isRight_iff, Option.isSome_iff_exists];
  simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru