English
Let s be a subset of the subtype { x // P x }. Then s is a lower set in this subtype iff the image of s under the projection to α is a RelLowerSet with respect to P.
Русский
Пусть s ⊆ { x // P x }. Тогда s является нижним множеством в этом субтипе тогда и только тогда, когда образ s под проекции на α является RelLowerSet относительно P.
LaTeX
$$$IsLowerSet s \;\iff\; IsRelLowerSet (Subtype.val '' s) P$$$
Lean4
theorem isLowerSet_subtype_iff_isRelLowerSet {s : Set { x // P x }} :
IsLowerSet s ↔ IsRelLowerSet (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 ⟨b, y⟩ ≤ a 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
