coe_inclusion — Mathlib

English

The inclusion map from S into A is the identity on S when viewed inside A; i.e., for every s ∈ S, the image of s under inclusion is just s considered as an element of A.

Русский

Отображение включения из S в A тождественно на S при рассмотрении элементов S как элементов A.

LaTeX

$$$\forall s \in S,\; \iota_h(s) = s$$$

Lean4

@[simp]
theorem coe_inclusion (s : S) : (inclusion h s : A) = s :=
  rfl

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