Semantic membership for arbitrary-format executable intervals

RealMem interprets a finite-endpoint interval as a closed interval in ℝ. ERealMem interprets its endpoints in EReal, so outward-rounded operations remain meaningful when a result overflows to an infinity. Meaningful endpoint interpretations require Valid or ValidExtended; the totalized decoders alone do not exclude NaN endpoints.

The executable interval carrier remains independent of these interpretations.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.RealMem {fmt : FloatFormat} (I : Interval fmt) (x : ℝ) : Prop

Membership in the real interval denoted by the decoded endpoints.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.ERealMem {fmt : FloatFormat} (I : Interval fmt) (x : EReal) : Prop

Membership in the extended-real interval denoted by the decoded endpoints.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.realMem_iff {fmt : FloatFormat} (I : Interval fmt) (x : ℝ) : I.RealMem x ↔ I.lo.toReal ≤ x ∧ x ≤ I.hi.toReal

Real membership unfolds to the two endpoint inequalities.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.eRealMem_iff {fmt : FloatFormat} (I : Interval fmt) (x : EReal) : I.ERealMem x ↔ I.lo.toEReal ≤ x ∧ x ≤ I.hi.toEReal

Extended-real membership unfolds to the two endpoint inequalities.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.Valid.lo_isFinite {fmt : FloatFormat} {I : Interval fmt} (hI : I.Valid) : I.lo.isFinite = true

The lower endpoint of a valid interval is finite.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.Valid.hi_isFinite {fmt : FloatFormat} {I : Interval fmt} (hI : I.Valid) : I.hi.isFinite = true

The upper endpoint of a valid interval is finite.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.Valid.ordered {fmt : FloatFormat} {I : Interval fmt} (hI : I.Valid) : I.lo.le I.hi

The endpoints of a valid interval are ordered by executable comparison.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.ValidExtended.lo_isNaN_eq_false {fmt : FloatFormat} {I : Interval fmt} (hI : I.ValidExtended) : I.lo.isNaN = false

The lower endpoint of an extended-valid interval is not a NaN.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.ValidExtended.hi_isNaN_eq_false {fmt : FloatFormat} {I : Interval fmt} (hI : I.ValidExtended) : I.hi.isNaN = false

The upper endpoint of an extended-valid interval is not a NaN.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.ValidExtended.ordered {fmt : FloatFormat} {I : Interval fmt} (hI : I.ValidExtended) : I.lo.le I.hi

The endpoints of an extended-valid interval are ordered numerically.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.Valid.validExtended {fmt : FloatFormat} {I : Interval fmt} (hI : I.Valid) : I.ValidExtended

Every finite valid interval is extended-valid.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.ValidExtended.valid_of_isFinite {fmt : FloatFormat} {I : Interval fmt} (hI : I.ValidExtended) (hlo : I.lo.isFinite = true) (hhi : I.hi.isFinite = true) : I.Valid

An extended-valid interval is finite-valid once both endpoints are known to be finite.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.eRealMem_coe_iff_of_valid {fmt : FloatFormat} {I : Interval fmt} (hI : I.Valid) (x : ℝ) : I.ERealMem ↑x ↔ I.RealMem x

For a valid interval, embedding real membership into EReal preserves membership exactly.