eq_of_mem_of_mem

Mathlib.Data.Option.Basic

URI: https://scilib.ai/kg/mathlib#Option.eq_of_mem_of_mem

English

If an element a belongs to both o1 and o2, then o1 and o2 are equal.

Русский

Если элемент a принадлежит o1 и o2, то o1 = o2.

LaTeX

$$$$ \forall a, o_1, o_2 : \mathrm{Option}\;\alpha, a \in o_1 \rightarrow a \in o_2 \rightarrow o_1 = o_2. $$$$

Lean4

theorem eq_of_mem_of_mem {a : α} {o1 o2 : Option α} (h1 : a ∈ o1) (h2 : a ∈ o2) : o1 = o2 :=
  h1.trans h2.symm

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

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

Разделы

Аффилиация

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