English
Let S and T be subsets of α with S ⊆ T. The inclusion map i_H: S → T is given by i_H(x) = x viewed as an element of T (equivalently i_H(x) = ⟨x, H x.2⟩). This is the natural embedding of S into T.
Русский
Пусть S и T — подмножества α и S ⊆ T. Включение i_H: S → T задаётся отображением i_H(x) = x как элемента T (то есть i_H(x) = ⟨x, H x.2⟩). Это естественное вложение S в T.
LaTeX
$$$s \subseteq t \Rightarrow \exists i: s \to t,\ \forall x \in s,\ i(x) = x.$$$
Lean4
/-- `inclusion` is the "identity" function between two subsets `s` and `t`, where `s ⊆ t` -/
abbrev inclusion (h : s ⊆ t) : s → t := fun x : s => (⟨x, h x.2⟩ : t)
