Lean4
/-- For a nonempty subset of a conditionally complete linear order to be a conditionally complete
linear order, it suffices that it contain the `sSup` of all its nonempty bounded-above subsets, and
the `sInf` of all its nonempty bounded-below subsets.
See note [reducible non-instances]. -/
noncomputable abbrev subsetConditionallyCompleteLinearOrder [Inhabited s]
(h_Sup : ∀ {t : Set s} (_ : t.Nonempty) (_h_bdd : BddAbove t), sSup ((↑) '' t : Set α) ∈ s)
(h_Inf : ∀ {t : Set s} (_ : t.Nonempty) (_h_bdd : BddBelow t), sInf ((↑) '' t : Set α) ∈ s) :
ConditionallyCompleteLinearOrder s :=
{ subsetSupSet s, subsetInfSet s, DistribLattice.toLattice,
(inferInstance :
LinearOrder
s) with
le_csSup := by
rintro t c h_bdd hct
rw [← Subtype.coe_le_coe, ← subset_sSup_of_within s ⟨c, hct⟩ h_bdd (h_Sup ⟨c, hct⟩ h_bdd)]
exact (Subtype.mono_coe _).le_csSup_image hct h_bdd
csSup_le := by
rintro t B ht hB
rw [← Subtype.coe_le_coe, ← subset_sSup_of_within s ht ⟨B, hB⟩ (h_Sup ht ⟨B, hB⟩)]
exact (Subtype.mono_coe s).csSup_image_le ht hB
le_csInf := by
intro t B ht hB
rw [← Subtype.coe_le_coe, ← subset_sInf_of_within s ht ⟨B, hB⟩ (h_Inf ht ⟨B, hB⟩)]
exact (Subtype.mono_coe s).le_csInf_image ht hB
csInf_le := by
rintro t c h_bdd hct
rw [← Subtype.coe_le_coe, ← subset_sInf_of_within s ⟨c, hct⟩ h_bdd (h_Inf ⟨c, hct⟩ h_bdd)]
exact (Subtype.mono_coe s).csInf_image_le hct h_bdd
csSup_of_not_bddAbove := fun t ht ↦ by simp [ht]
csInf_of_not_bddBelow := fun t ht ↦ by simp [ht] }
