mem_ofOption — Mathlib

English

For a fixed a, for any o : Option α, a ∈ ofOption o ↔ a ∈ o.

Русский

Для фиксированного a, для любого o : Option α, a ∈ ofOption o ⇔ a ∈ o.

LaTeX

$$$ a \in \mathrm{ofOption}(o) \iff a \in o $$$

Lean4

@[simp]
theorem mem_ofOption {a : α} : ∀ {o : Option α}, a ∈ ofOption o ↔ a ∈ o
  | Option.none => ⟨fun h => h.fst.elim, fun h => Option.noConfusion h⟩
  | Option.some _ => ⟨fun h => congr_arg Option.some h.snd, fun h => ⟨trivial, Option.some.inj h⟩⟩

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