ofOption_dom — Mathlib

English

The domain of ofOption o is equivalent to o.isSome; i.e., (ofOption o).Dom holds exactly when o is some.

Русский

Область определения ofOption o эквивалентна o.isSome; то есть (ofOption o).Dom истинно тогда и только тогда, когда o является some.

LaTeX

$$$ (\\mathrm{ofOption}(o)).\\Dom \\Leftrightarrow o.\\isSome $$$

Lean4

@[simp]
theorem ofOption_dom {α} : ∀ o : Option α, (ofOption o).Dom ↔ o.isSome
  | Option.none => by simp [ofOption, none]
  | Option.some a => by simp [ofOption]

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