ofSet_eq_some_self_iff — Mathlib

English

Let s be a subset of α. The partial equivalence determined by s maps a to Some a exactly when a ∈ s.

Русский

Пусть s ⊆ α. Частичное эквивалентное отображение, задаваемое s, возвращает a тогда, когда a ∈ s.

LaTeX

$$$(\\operatorname{ofSet} s) a = \\operatorname{Some} a \\Leftrightarrow a \\in s$$$

Lean4

theorem ofSet_eq_some_self_iff {s : Set α} {_ : DecidablePred (· ∈ s)} {a : α} : ofSet s a = some a ↔ a ∈ s :=
  mem_ofSet_self_iff

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