English
Let p : α → Prop, q : β → Prop, f,g : α → β with h1 : ∀a, p a → q(f a) and h2 : ∀a, p a → q(g a). For x,y : Subtype p, the equality of their images under (map f h1) and (map g h2) is equivalent to equality of the underlying images: (Subtype.map f h1 x) = (Subtype.map g h2 y) iff f x.val = g y.val.
Русский
Пусть p : α → Prop, q : β → Prop, f,g : α → β и h1 : ∀a, p(a) → q(f(a)), h2 : ∀a, p(a) → q(g(a)). Для x,y : Subtype p верно: отображения x и y в Subtype β через f и g совпадают тогда и только тогда, когда их значения совпадают: (Subtype.map f h1 x) = (Subtype.map g h2 y) ↔ f(x.val) = g(y.val).
LaTeX
$$$\forall {x y : \{ a : \alpha \mid p(a) \}},\ (\operatorname{Subtype.map} f h_1\, x) = (\operatorname{Subtype.map} g h_2\, y) \iff f(x.\text{val}) = g(y.\text{val}).$$$
Lean4
theorem map_eq {p : α → Prop} {q : β → Prop} {f g : α → β} (h₁ : ∀ a : α, p a → q (f a)) (h₂ : ∀ a : α, p a → q (g a))
{x y : Subtype p} : map f h₁ x = map g h₂ y ↔ f x = g y :=
Subtype.ext_iff
