equivSubtype_symm_trans_valEmbedding

English

The natural equivalence between Fin n and the subtype {x ∈ ℕ | x < n} implies that the reverse embedding composed with the natural inclusion to ℕ equals the standard subtype embedding.

Русский

Естественное эквивалентное отображение между Fin n и подтипом {x ∈ ℕ | x < n} означает, что обратное вложение, составленное с естественным включением в ℕ, равно стандартному вложению подтипа.

LaTeX

$$$ \mathrm{equivSubtype}^{-1} \toEmbedding \mathrm{trans} \mathrm{valEmbedding} = \mathrm{Embedding.subtype} (\cdot < n)$$$

Lean4

@[simp]
theorem equivSubtype_symm_trans_valEmbedding :
    equivSubtype.symm.toEmbedding.trans valEmbedding = Embedding.subtype (· < n) :=
  rfl

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