English
For p, q predicates and f: α → β with h: ∀x, p x → q (f x), the range of Subtype.map f h equals the preimage under Subtype.val of the image of f on {x | p x}.
Русский
Для предикатов p, q и отображения f с данными условием h, отображение Subtype.map f h охватывает те значения, которые являются образами f на множествах с p
LaTeX
$$$\operatorname{range}(\operatorname{Subtype.map} f h) = (\uparrow)^{-1}(f '' \{ x \mid p x \})$$$
Lean4
theorem range_subtype_map {p : α → Prop} {q : β → Prop} (f : α → β) (h : ∀ x, p x → q (f x)) :
range (Subtype.map f h) = (↑) ⁻¹' (f '' {x | p x}) :=
by
ext ⟨x, hx⟩
simp_rw [mem_preimage, mem_range, mem_image, Subtype.exists, Subtype.map]
simp only [Subtype.mk.injEq, exists_prop, mem_setOf_eq]
