out — Mathlib

English

There is an embedding out : hs.Quotient ↪ α that chooses a representative for each quotient class, using hs.some.

Русский

Существует вложение out : hs.Quotient ↪ α, выбирающее представителя для каждого класса эквивалентности, с помощью hs.some.

LaTeX

$$$ out : hs.Quotient \hookrightarrow α $$$

Lean4

/-- A map choosing a representative for each element of the quotient associated to an indexed
partition. This is a computable version of `Quotient.out` using `IndexedPartition.some`. -/
def out : hs.Quotient ↪ α :=
  hs.equivQuotient.symm.toEmbedding.trans ⟨hs.some, Function.LeftInverse.injective hs.index_some⟩

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