coe_eq_subtype — Mathlib

English

For any subset S of a type α, the subtype of α consisting of elements of S is exactly the same object as the collection { x ∈ α | x ∈ S }, i.e., the canonical identification between the elements of S and the elements of α that lie in S.

Русский

Для произвольного подмножества S множества α существует каноническое равенство между подтипом S и множеством { x ∈ α | x ∈ S }, то есть между элементами подтипа и элементами α, принадлежащими S.

LaTeX

$$$\uparrow s = \{ x \in \alpha \mid x \in s \}$$$

Lean4

theorem coe_eq_subtype (s : Set α) : ↥s = { x // x ∈ s } :=
  rfl

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