← Copula mathematical handbook

@[instance_reducible]

instance Std.PRange.instUpwardEnumerableNat : UpwardEnumerable Nat

Equations

• Std.PRange.instUpwardEnumerableNat = { succ? := fun (n : Nat) => some (n + 1), succMany? := fun (k n : Nat) => some (n + k) }

@[instance_reducible]

instance Std.PRange.instLeast?Nat : Least? Nat

Equations

• Std.PRange.instLeast?Nat = { least? := some 0 }

instance Std.PRange.instLawfulUpwardEnumerableLeast?Nat : LawfulUpwardEnumerableLeast? Nat

instance Std.PRange.instLawfulUpwardEnumerableLENat : LawfulUpwardEnumerableLE Nat

instance Std.PRange.instLawfulUpwardEnumerableNat : LawfulUpwardEnumerable Nat

instance Std.PRange.instLawfulUpwardEnumerableLTNat : LawfulUpwardEnumerableLT Nat

instance Std.PRange.instInfinitelyUpwardEnumerableNat : InfinitelyUpwardEnumerable Nat

@[instance_reducible]

instance Std.PRange.instHasSizeNat : Rxc.HasSize Nat

Equations

• Std.PRange.instHasSizeNat = { size := fun (lo hi : Nat) => hi + 1 - lo }

@[instance_reducible]

instance Std.PRange.instHasSizeNat_1 : Rxo.HasSize Nat

Equations

• Std.PRange.instHasSizeNat_1 = Std.Rxo.HasSize.ofClosed

instance Std.PRange.instLawfulHasSizeNat : Rxc.LawfulHasSize Nat

instance Std.PRange.instIsAlwaysFiniteNat : Rxc.IsAlwaysFinite Nat

instance Std.PRange.instLawfulHasSizeNat_1 : Rxo.LawfulHasSize Nat

instance Std.PRange.instIsAlwaysFiniteNat_1 : Rxo.IsAlwaysFinite Nat

instance Std.PRange.instLinearlyUpwardEnumerableNat : LinearlyUpwardEnumerable Nat

@[instance_reducible]

instance Std.instHasRcoIntersectionNat : Roo.HasRcoIntersection Nat

Equations

• Std.instHasRcoIntersectionNat = { intersection := fun (r : Std.Roo Nat) (s : Std.Rco Nat) => (max (r.lower + 1) s.lower)...min r.upper s.upper }

instance Std.instLawfulRcoIntersectionNat : Roo.LawfulRcoIntersection Nat

@[instance_reducible]

instance Std.instHasRcoIntersectionNat_1 : Roc.HasRcoIntersection Nat

Equations

• Std.instHasRcoIntersectionNat_1 = { intersection := fun (r : Std.Roc Nat) (s : Std.Rco Nat) => (max (r.lower + 1) s.lower)...min (r.upper + 1) s.upper }

instance Std.instLawfulRcoIntersectionNat_1 : Roc.LawfulRcoIntersection Nat

@[instance_reducible]

instance Std.instHasRcoIntersectionNat_2 : Roi.HasRcoIntersection Nat

Equations

• Std.instHasRcoIntersectionNat_2 = { intersection := fun (r : Std.Roi Nat) (s : Std.Rco Nat) => (max (r.lower + 1) s.lower)...s.upper }

instance Std.instLawfulRcoIntersectionNat_2 : Roi.LawfulRcoIntersection Nat

@[instance_reducible]

instance Std.instHasRcoIntersectionNat_3 : Rco.HasRcoIntersection Nat

Equations

• Std.instHasRcoIntersectionNat_3 = { intersection := fun (r s : Std.Rco Nat) => (max r.lower s.lower)...min r.upper s.upper }

instance Std.instLawfulRcoIntersectionNat_3 : Rco.LawfulRcoIntersection Nat

@[instance_reducible]

instance Std.instHasRcoIntersectionNat_4 : Rcc.HasRcoIntersection Nat

Equations

• Std.instHasRcoIntersectionNat_4 = { intersection := fun (r : Std.Rcc Nat) (s : Std.Rco Nat) => (max r.lower s.lower)...min (r.upper + 1) s.upper }

instance Std.instLawfulRcoIntersectionNat_4 : Rcc.LawfulRcoIntersection Nat

@[instance_reducible]

instance Std.instHasRcoIntersectionNat_5 : Rci.HasRcoIntersection Nat

Equations

• Std.instHasRcoIntersectionNat_5 = { intersection := fun (r : Std.Rci Nat) (s : Std.Rco Nat) => (max r.lower s.lower)...s.upper }

instance Std.instLawfulRcoIntersectionNat_5 : Rci.LawfulRcoIntersection Nat

@[instance_reducible]

instance Std.instHasRcoIntersectionNat_6 : Rio.HasRcoIntersection Nat

Equations

• Std.instHasRcoIntersectionNat_6 = { intersection := fun (r : Std.Rio Nat) (s : Std.Rco Nat) => s.lower...min r.upper s.upper }

instance Std.instLawfulRcoIntersectionNat_6 : Rio.LawfulRcoIntersection Nat

@[instance_reducible]

instance Std.instHasRcoIntersectionNat_7 : Ric.HasRcoIntersection Nat

Equations

• Std.instHasRcoIntersectionNat_7 = { intersection := fun (r : Std.Ric Nat) (s : Std.Rco Nat) => s.lower...min (r.upper + 1) s.upper }

instance Std.instLawfulRcoIntersectionNat_7 : Ric.LawfulRcoIntersection Nat