isSome_getLeft?_iff_isLeft

Mathlib.Data.Sum.Basic

URI: https://scilib.ai/kg/mathlib#Sum.isSome_getLeft?_iff_isLeft

English

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

Русский

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

LaTeX

$$@[simp]\n\text{theorem isSome_getLeft?_iff_isLeft} : x.getLeft?.isSome \iff x.isLeft$$

Lean4

@[simp]
theorem isSome_getLeft?_iff_isLeft : x.getLeft?.isSome ↔ x.isLeft := by rw [isLeft_iff, Option.isSome_iff_exists]; simp

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

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

Разделы

Аффилиация

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