leftUnique

Mathlib.Data.Option.Basic

URI: https://scilib.ai/kg/mathlib#Option.Mem.leftUnique

English

For any x, if x belongs to two options y1 and y2, then y1 = y2.

Русский

Для любого x, если x принадлежит двум значениям y1 и y2, то y1 = y2.

LaTeX

$$$$ \forall x: \alpha, \forall y_1, y_2 : \mathrm{Option}\; \alpha, (x \in y_1) \land (x \in y_2) \Rightarrow y_1 = y_2. $$$$

Lean4

theorem leftUnique : Relator.LeftUnique ((· ∈ ·) : α → Option α → Prop) := fun _ _ _ => mem_unique

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

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

Разделы

Аффилиация

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