English
Let s be a subset of α and t ⊆ s be a subset of s. Then the underlying α-set of t (viewed via the first projection) coincides with the image of t under that projection; equivalently, the projection of t to α equals the set of first coordinates of elements of t.
Русский
Пусть s ⊆ α, и пусть t ⊆ s. Тогда множество первых координат элементов t совпадает с образом t по проекции тa на α; то есть проекция t на α равна множеству первых координат элементов t.
LaTeX
$$$\operatorname{image} \operatorname{Subtype.val} t = \{ a \in \alpha \mid \exists x \in t, \operatorname{val}(x) = a \}. $$$
Lean4
/-- The coercion from `Set.monad` as an instance is equal to the coercion in `Data.Set.Notation`. -/
theorem coe_eq_image_val (t : Set s) : @Lean.Internal.coeM Set s α _ _ t = Subtype.val '' t :=
by
change ⋃ (x ∈ t), { x.1 } = _
ext
simp
