subsingleton_coe_of_subsingleton — Mathlib

English

If α is a subsingleton, then the coe of any set s is a subsingleton.

Русский

Если α является подсинглтоном, то копия типа множества s через приведение к типу является подсинглтоном.

LaTeX

$$$ [Subsingleton \alpha] \; {s : Set \alpha} : Subsingleton s :=$$

Lean4

/-- The `coe_sort` of a set `s` in a subsingleton type is a subsingleton.
For the corresponding result for `Subtype`, see `subtype.subsingleton`. -/
instance subsingleton_coe_of_subsingleton [Subsingleton α] {s : Set α} : Subsingleton s :=
  by
  rw [s.subsingleton_coe]
  exact subsingleton_of_subsingleton

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