eq_left_iff_getLeft_eq

Mathlib.Data.Sum.Basic

URI: https://scilib.ai/kg/mathlib#Sum.eq_left_iff_getLeft_eq

English

For any a, x, the equation x = inl a is equivalent to the existence of h with x.getLeft h = a.

Русский

Для любого a и x справедливо: x = inl a эквивалентно существованию h such that x.getLeft h = a.

LaTeX

$$$\forall {a : \alpha},\ x = \mathrm{inl} a \iff \exists h,\ x.getLeft h = a$$$

Lean4

theorem eq_left_iff_getLeft_eq {a : α} : x = inl a ↔ ∃ h, x.getLeft h = a := by cases x <;> simp

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

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

Разделы

Аффилиация

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