Set.uIoo

Stream: Is there code for X?

[Alex Kontorovich]

I see lots of API for Set.uIcc and Set.uIoc, but no Set.uIoo? Is there a reason for this?

[Yaël Dillies]

Nobody needed it. If you do need it, I can add the API quickly.

[Alex Kontorovich]

That'd be great, thanks! (I didn't know if that was a design choice, or if I was supposed to use something else for this case...)

[Alex Kontorovich]

Here's a use case (that I could use some help with please): I know something on an open interval, and want to derive that it's true for almost all points on the closed interval:

import Mathlib
open scoped Interval

example (a b : ℝ) (hab : a < b) (p : ℝ → Prop) (h : ∀ x ∈ Set.Ioo a b, p x) :
    ∀ᵐ (x : ℝ) ∂MeasureTheory.volume, x ∈ [[a, b]] → p x := by sorry

[Alex Kontorovich]

(Of course I would like to drop the a < b assumption and use uIoo instead...)

[Yaël Dillies]

Oh, I see. In the meantime you can always use Set.Ioo (min a b) (max a b).

[Yaël Dillies]

I write Lean code fast but not instantaneously :wink: (and I'm currently working at making some more of https://yaeldillies.github.io/LeanAPAP/blueprint/dep_graph_document green)

[Alex Kontorovich]

No rush of course! :) (A hint on the second question would be higher priority...)

[Yaël Dillies]

I would do it low-brow by proving that {x | x ∈ [[a, b]] → p x}ᶜ ⊆ {a, b} and that μ {a, b} = 0.