IsLowerSet.Iio_csSup_subset

Stream: Is there code for X?

[Violeta Hernández]

Am I missing something? I found docs#IsPreconnected.Iio_csSup_subset, but the theorem that lower sets are preconnected doesn't seem to exist. (Besides, I don't think this result requires any topology?)

[Violeta Hernández]

Ah, so what I want is to chain together the theorems IsLowerSet.ordConnected, and OrdConnected.isPreconnected, and IsPreconnected.Iio_csSup_subset.

[Violeta Hernández]

This does feel backwards. I don't think IsLowerSet.Iio_csSup_subset should require anything but a conditionally complete linear order.

[Violeta Hernández]

Really frustrating how hard this has been to find. The argument of "take an element slightly smaller than the supremum, thus it's in the set" is a standard one in elementary real analysis.

[Jireh Loreaux]

I think I would do this via docs#IsLUB.biUnion_Iio_eq and docs#IsLowerSet.Iio_subset

[Jireh Loreaux]

import Mathlib

open Set

variable {α : Type*} [ConditionallyCompleteLinearOrder α] (s : Set α)

example (hs : IsLowerSet s) (hs_non : s.Nonempty) (hs_bdd : BddAbove s) :
    Iio (sSup s) ⊆ s := by
  simpa [← (isLUB_csSup hs_non hs_bdd).biUnion_Iio_eq, iUnion₂_subset_iff] using hs.Iio_subset

[Jireh Loreaux]

In particular, it's docs#IsLUB.biUnion_Iio_eq which is the "take an element slightly smaller than the supremum" bit.