orElse_eq_none — Mathlib

English

Let o, o' be elements of an Option-type. Then the left-biased combination o <|> o' equals none exactly when both o and o' are none.

Русский

Пусть o и o' — элементы типа Option. Тогда их объединение через лево-ориентированное «или» равно none тогда, когда оба равны none.

LaTeX

$$$ (o \oplus o') = \mathrm{none} \iff o = \mathrm{none} \land o' = \mathrm{none} $$$

Lean4

theorem orElse_eq_none (o o' : Option α) : (o <|> o') = none ↔ o = none ∧ o' = none := by simp

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