mem_toOption — Mathlib

English

For any o ∈ Part α, a ∈ toOption(o) iff a ∈ o.

Русский

Для любого o ∈ Part α, a ∈ toOption(o) ⇔ a ∈ o.

LaTeX

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

Lean4

theorem mem_toOption {o : Part α} [Decidable o.Dom] {a : α} : a ∈ toOption o ↔ a ∈ o :=
  by
  unfold toOption
  by_cases h : o.Dom
  · simpa [h] using ⟨fun h => ⟨_, h⟩, fun ⟨_, h⟩ => h⟩
  · simp only [h, ↓reduceDIte, Option.mem_def, reduceCtorEq, false_iff]
    exact mt Exists.fst h

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