orElse_eq_some — Mathlib

English

The orElse operation o <|> o' yields some x exactly when either o = some x or (o = none and o' = some x).

Русский

Операция orElse o <|> o' возвращает some x тогда, когда либо o = some x, либо o = none и o' = some x.

LaTeX

$$$$ (o <|> o') = \mathrm{some}(x) \iff o = \mathrm{some}(x) \lor (o = \mathrm{none} \land o' = \mathrm{some}(x)). $$$$

Lean4

theorem orElse_eq_some (o o' : Option α) (x : α) : (o <|> o') = some x ↔ o = some x ∨ o = none ∧ o' = some x := by simp

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