English
Let s be a subset of the subtype { x // P x }. Then s is an upper set in this subtype iff the image of s under the projection to α is a RelUpperSet with respect to P.
Русский
Пусть s ⊆ { x // P x }. Тогда s является верхним множеством в этом субтипе тогда и только тогда, когда образ s под проекции на α является RelUpperSet относительно P.
LaTeX
$$$IsUpperSet s \;\iff\; IsRelUpperSet (Subtype.val '' s) P$$$
Lean4
theorem isUpperSet_subtype_iff_isRelUpperSet {s : Set { x // P x }} :
IsUpperSet s ↔ IsRelUpperSet (Subtype.val '' s) P :=
by
refine ⟨fun h a x ↦ ?_, fun h a b x y ↦ ?_⟩
· obtain ⟨a, ma, rfl⟩ := x
exact ⟨a.2, fun b x y ↦ by simpa [h (show a ≤ ⟨b, y⟩ by exact x) ma]⟩
· have ma : a.1 ∈ Subtype.val '' s := by simp [a.2, y]
simpa only [mem_image, SetCoe.ext_iff, exists_eq_right] using (h ma).2 x b.2
