Initialization for the dyadic real interval extension family

This file initializes the interval_dyadic_real inclusion family and defines the ToSet, Univ and Coarsen instances it uses in the inclusion tactic.

opaque Inclusion.IntervalDyadicReal.intervalDyadicRealFamily : InclusionFamily

Initializes the interval_dyadic_real inclusion family.

@[instance_reducible]

instance Inclusion.IntervalDyadicReal.instToSetIntervalDyadicReal : ToSet (Interval Dyadic) ℝ

Equations

• Inclusion.IntervalDyadicReal.instToSetIntervalDyadicReal = { toSet := fun (I : Inclusion.Interval Dyadic) => (I.map Dyadic.toReal).toSet }

@[instance_reducible]

instance Inclusion.IntervalDyadicReal.instUnivIntervalDyadicReal : Univ (Interval Dyadic) ℝ

Equations

• Inclusion.IntervalDyadicReal.instUnivIntervalDyadicReal = { univ := Inclusion.Interval.univ Dyadic, mem_univ := ⋯ }

@[instance_reducible]

instance Inclusion.IntervalDyadicReal.instRefineIntervalDyadicReal : Refine (Interval Dyadic) ℝ

Equations

• Inclusion.IntervalDyadicReal.instRefineIntervalDyadicReal = { refine := Inclusion.Interval.inter, mem_refine := ⋯ }

@[instance_reducible]

instance Inclusion.IntervalDyadicReal.instCoarsenIntervalDyadicReal : Coarsen (Interval Dyadic) ℝ

Equations

• Inclusion.IntervalDyadicReal.instCoarsenIntervalDyadicReal = { coarsen := Inclusion.Interval.hull, mem_coarsen_left := ⋯, mem_coarsen_right := ⋯ }