ofSet_eq_some_iff — Mathlib

English

For ofSet, the equation of the output to some value corresponds to a being equal to that value and belonging to s.

Русский

Для ofSet равенство некоторого значения совпадает с тем, что a совпадает с b и a ∈ s.

LaTeX

$$$$ \\mathrm{ofSet}(s)\\, b = \\text{some } a \\iff a = b \\land a \\in s. $$$$

Lean4

@[simp]
theorem ofSet_eq_some_iff {s : Set α} {_ : DecidablePred (· ∈ s)} {a b : α} : ofSet s b = some a ↔ a = b ∧ a ∈ s :=
  mem_ofSet_iff

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