English
On an OrdConnected subset s of α, there is a PredOrder structure on s given by a constructive pullback from α.
Русский
На OrdConnected-подмножестве s кучается PredOrder на s, получаемый линейным переносом из α.
LaTeX
$$$$ [PredOrder\s.Elem] \\text{ on } s \\text{ via } \text{Subtype} \toPreorder \text{ using } s.OrdConnected \text{ and } PredOrder. $$$$
Lean4
noncomputable instance predOrder [PredOrder α] : PredOrder s
where
pred x := if h : Order.pred x.1 ∈ s then ⟨Order.pred x.1, h⟩ else x
pred_le := fun ⟨x, hx⟩ ↦ by dsimp; split <;> simp_all [Order.pred_le]
min_of_le_pred :=
@fun ⟨x, hx⟩ h ↦ by
dsimp at h
split_ifs at h with h'
· simp only [Subtype.mk_le_mk, Order.le_pred_iff_isMin] at h
rintro ⟨y, _⟩ hy
simp [h hy]
· rintro ⟨y, hy⟩ h
rcases h.lt_or_eq with h | h
· simp only [Subtype.mk_lt_mk] at h
have := h.le_pred
absurd h'
apply out' hy hx
simp [this, Order.pred_le]
· simp [h]
le_pred_of_lt :=
@fun ⟨b, hb⟩ ⟨c, hc⟩ h ↦ by
rw [Subtype.mk_lt_mk] at h
dsimp only
split
· exact h.le_pred
· exact h.le
