coeEmb — Mathlib

English

There is a natural order-embedding of finite subsets into subsets of the ambient set, given by viewing a finite subset as its carrier.

Русский

Существует естественное вложение в порядок от конечных подмножеств в множества, задаваемое восприятием подмножества как множества его элементов.

LaTeX

$$$\exists e:\mathrm{Finset}(\alpha) \hookrightarrow_o \mathrm{Set}(\alpha),\; e(S) = S\text{ (as a subset of }\alpha\text{)}$$$

Lean4

/-- Coercion to `Set α` as an `OrderEmbedding`. -/
def coeEmb : Finset α ↪o Set α :=
  ⟨⟨(↑), coe_injective⟩, coe_subset⟩

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