setOf_set — Mathlib

English

The set of a set s, i.e., setOf s, is equal to s; this is a definitional equality between the encoding of a set as a predicate and as a set.

Русский

Набор множества setOf s равен самому множеству s; это дефиниционное равенство между кодировкой множества как предиката и как множества.

LaTeX

$$$\text{setOf } s = s$$$

Lean4

@[deprecated "This lemma abuses the `Set α := α → Prop` defeq.
      If you think you need it you have already taken a wrong turn." (since := "2025-06-10")]
theorem setOf_set {s : Set α} : setOf s = s :=
  rfl

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